Tag Archives: sphere eversion
Lean 2022 round-up
A brief survey post containing some of the things which happened in the Lean community in 2022. The Liquid Tensor Experiment In December 2020, Fields Medallist Peter Scholze challenged the formal computer proof community to verify one of his theorems … Continue reading
Posted in Uncategorized
Tagged Johan Commelin, liquid tensor experiment, Patrick Massot, Peter Scholze, sphere eversion
4 Comments
The Sphere Eversion Project
Patrick Massot has written a blueprint for sphere eversion. This marks the beginning of a community formalisation project. Continue reading
Posted in Imperial, Learning Lean, Type theory
Tagged cap set, Johannes Hölzl, Patrick Massot, perfectoid space, Rob Lewis, Sander Dahmen, scheme, sphere eversion
2 Comments
Xena 