Formal Proof of Banach-Tarski Paradox

Daniel de Rauglaudre


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.

Full Text:

PDF (English)


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].

DOI: 10.6092/issn.1972-5787/6927

Copyright (c) 2017 Daniel de Rauglaudre

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.