@article{de Rauglaudre_2017, title={Formal Proof of Banach-Tarski Paradox}, volume={10}, url={https://jfr.unibo.it/article/view/6927}, DOI={10.6092/issn.1972-5787/6927}, abstractNote={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.}, number={1}, journal={Journal of Formalized Reasoning}, author={de Rauglaudre, Daniel}, year={2017}, month={Jan.}, pages={37–49} }