Zulip Chat Archive

Stream: maths

Topic: Banach-Tarski Paradox


view this post on Zulip James Palmer (Aug 11 2020 at 14:29):

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

view this post on Zulip Alex J. Best (Aug 11 2020 at 14:50):

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.

view this post on Zulip Bryan Gin-ge Chen (Aug 11 2020 at 15:07):

@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


Last updated: May 18 2021 at 08:14 UTC