3 ms·
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 i
by Smaug123 6y ago
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).
https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph.html https://leanprover-community.github.io/sphere-eversion/bluep...
- kmill 6y agoYeah, 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.