Formal Proof of Banach-Tarski Paradox
de Rauglaudre, Daniel
Journal of Formalized Reasoning, Volume 10 (2017), / Harvested from Journal of Formalized Reasoning

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.

Published online : 2017-01-01
DOI : https://doi.org/10.6092/issn.1972-5787/6927
@article{6927,
     title = {Formal Proof of Banach-Tarski Paradox},
     journal = {Journal of Formalized Reasoning},
     volume = {10},
     year = {2017},
     doi = {10.6092/issn.1972-5787/6927},
     language = {EN},
     url = {http://dml.mathdoc.fr/item/6927}
}
de Rauglaudre, Daniel. Formal Proof of Banach-Tarski Paradox. Journal of Formalized Reasoning, Volume 10 (2017) . doi : 10.6092/issn.1972-5787/6927. http://gdmltest.u-ga.fr/item/6927/