Xena

Mathematicians learning Lean by doing.

Skip to content

Home
About Xena
Student projects
What maths is in Lean?
Installing Lean and mathlib
Twitter
Useful links.

Tag Archives: Jeremy Avigad

Lean Together 2020

Posted on January 14, 2020 by xenaproject

Thoughts on the talks at FoMM/Lean Together 2020 Continue reading →

Posted in General | Tagged Jeremy Avigad, Lean 4, Lean together, Peter Koepke, Tom Hales | 1 Comment

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 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

Search for:
Categories

Recent Posts
- Lean 2022 round-up January 8, 2023
- Beyond the Liquid Tensor Experiment September 12, 2022
- The Future of Interactive Theorem Proving? August 16, 2022
- Teaching formalisation to mathematics undergraduates July 29, 2022
- 2022 Xena Project undergraduate workshop May 23, 2022

Create a free website or blog at WordPress.com.

Privacy & Cookies: This site uses cookies. By continuing to use this website, you agree to their use.
To find out more, including how to control cookies, see here: Cookie Policy

Follow Following
- Xena
- Already have a WordPress.com account? Log in now.