de Rauglaudre, D. Formal Proof of Banach-Tarski Paradox. JFR 2017, 10, 37-49.