Hello, Has any one formalized the Banach-Tarski decomposition (the "paradox" that you can make multiple spheres from one sphere) already? Would it be difficult? (I think in Mizar it would be much easier to formalize than in the other systems, and it would make a nice showcase.) Freek