The Banach–Tarski Paradox in Isabelle/HOL

We formalise in Isabelle/HOL the classical Banach–Tarski paradox for the closed unit ball in three-dimensional Euclidean space. The development proves the free-group paradox, the free subgroup of SO(3), the Hausdorff paradox away from a countable bad set, the absorption arguments for the sphere and the origin, and the final finite-partition theorem for the ball. The proof follows the standard route: the paradoxical decompo sition of the free group on two generators F2, the existence of a free subgroup F2 ≤ SO(3) via the AFP Free-Groups entry, the Hausdorff paradox for S2 \ D where D is a countable set of fixed points, and absorption arguments extending the partition to S2, then radially to B3\{0}, and finally to B3 itself. The argument crucially relies on the axiom of choice.