This paper presents a formal proof of the Banach-Tarski theorem in ACL2(r). The Banach-Tarski theorem states that a unit ball can be partitioned into a finite number of pieces that can be rotated to form two identical copies of the ball. We have formalized 3-D rotations and generated a free group of 3-d rotations of rank 2. The non-denumerability of the reals has been proved in ACL2(r) and the Axiom of Choice with the strengthen option has been introduced in ACL2 version 3.1. Using the free group of rotations, the Axiom of Choice, and the proof of the non-denumerability of reals, first we show that the unit sphere can be decomposed into two sets, each equivalent to the original sphere. Then we show that the unit ball except for the origin can be decomposed into two sets each equivalent to the original ball by mapping points of the unit ball to the points on the sphere. Finally, we handle the origin by rotating it around an axis such that the origin falls inside the sphere thus creating the two copies of the unit ball.