D. de Rauglaudre, “Formal Proof of Banach-Tarski Paradox”, JFR, vol. 10, no. 1, pp. 37–49, Jan. 2017.