de Rauglaudre, D. “Formal Proof of Banach-Tarski Paradox”. Journal of Formalized Reasoning, vol. 10, no. 1, Jan. 2017, pp. 37-49, doi:10.6092/issn.1972-5787/6927.