Tag Archives: Patrick Massot

Lean 2022 round-up

Posted on January 8, 2023 by xenaproject

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 , , , , | 4 Comments

The Sphere Eversion Project

Posted on June 5, 2020 by xenaproject

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 , , , , , , , | 2 Comments

Lean does not (yet) have real manifolds.

Posted on July 17, 2019 by xenaproject

Lean does not yet have real manifolds, but there has been recent progress. Continue reading →

Posted in General, Imperial, undergrad maths | Tagged , , , , , , , , , , , , , , , , | 7 Comments

Perfectoid spaces!

Posted on May 11, 2019 by xenaproject

Patrick Massot, Johan Commelin and I finished our definition of a perfectoid space in Lean! Patrick and Johan are professional mathematicians like me, not Imperial undergraduates, but I am sufficiently excited about the project that I couldn’t stop myself blogging … Continue reading →

Posted in Uncategorized | Tagged , , , , , | 4 Comments