Formal Proof of Banach-Tarski Paradox


  • Daniel de Rauglaudre Inria, Paris, France



Banach-Tarski Paradox states that a ball in 3D space is equidecomposable with twice itself, i.e. we can break a ball into a finite number of pieces, and with these pieces, build two balls having the same size as the initial ball. This strange result is actually a Theorem which was proven in 1924 by Stefan Banach and Alfred Tarski using the Axiom of Choice.

We present here a formal proof in Coq of this theorem.


Radu Diaconescu. Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51(1):176–178, 1975.

The Coq Development Team. The Coq proof assistant reference manual. PiR2 Team, 2017. Version 8.6.

Stan Wagon. The Banach-Tarski Paradox. Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1993.

Benjamin Werner. Sets in types, types in sets. In TACS, volume 1281 of Lecture Notes in Computer Science, pages 530–346. Springer, 1997.

Wikipedia. Banach-Tarski paradox — Wikipedia, the free encyclopedia, 2017. [Online; accessed 16-Apr-2017].

Wikipedia. Diaconescu’s theorem — Wikipedia, the free encyclopedia, 2017. [Online; accessed 20-Apr-2017].

Wikipedia. Hilbert’s paradox of the grand hotel — Wikipedia, the free encyclopedia, 2017. [Online; accessed 17-Apr-2017].




How to Cite

de Rauglaudre, D. (2017). Formal Proof of Banach-Tarski Paradox. Journal of Formalized Reasoning, 10(1), 37–49.