Banach-Tarski Paradox

Stream: maths

[James Palmer]

Hi everyone, I was wondering whether the Banach-Tarski paradox in Lean? Many thanks in advance!

[Alex J. Best]

I don't think anyone has. Someone did it in coq https://hal.archives-ouvertes.fr/hal-01673378 but it sounds like doing so was a significant effort.

[Bryan Gin-ge Chen]

@Ryan Lahfa asked about it a few months ago but I don't know if they started it: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/WIP.3A.20metric.20spaces.20tutorial/near/193088370