Tag Archives: Johan Commelin
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
Lean does not (yet) have real manifolds.
Lean does not yet have real manifolds, but there has been recent progress. Continue reading
Posted in General, Imperial, undergrad maths
Tagged Agda, Bochner Integral, Coq, HOL-Light, Idris, Isabelle-HOL, Jeremy Avigad, Johan Commelin, lean, manifold, Mizar, Patrick Massot, Perfectoid Spaces, Sebastien Gouezel, theorem provers, UniMath, Zhouhang Zhou
7 Comments
Perfectoid spaces!
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 Chris Hughes, Johan Commelin, Kenny Lau, Patrick Massot, perfectoid space, Ramon Fernandez Mir
4 Comments
Xena 