Re:Sphere Eversion
by Smaug123 on Saturday July 04, 2020 @02:13AM
(#23730505)
There's a proof project taking place in the Lean theorem prover right now! I don't know whether the method is the same as that in the article (I'm pretty sure it's not).
Re:Sphere Eversion
by kmill on Saturday July 04, 2020 @02:52AM
(#23730635)
Yeah, it's not. They're following something like Smale's proof as best as I understand. It will give some general useful topological tools for mathlib.
https://leanprover-community.github.io/sphere-eversion/bluep...