TY - JOUR
AU - de Rauglaudre, Daniel
PY - 2017/01/01
Y2 - 2022/01/28
TI - Formal Proof of Banach-Tarski Paradox
JF - Journal of Formalized Reasoning
JA - JFR
VL - 10
IS - 1
SE - Articles
DO - 10.6092/issn.1972-5787/6927
UR - https://jfr.unibo.it/article/view/6927
SP - 37 - 49
AB - 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.
ER -