constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Lean is a proof assistant based on dependent type theory. Like Rocq and Agda, it may be used to implement homotopy type theory.
Some mathematics that has been formalized in Lean (in particular in the Xena project):
basic synthetic mathematics homotopy theory (HoTT)
The main theorem of liquid vector spaces
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
1lab (cross-linked reference resource)
based on modal type theory:
based on simplicial type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Rocq)
UniMath project (using Rocq and Agda)
Xena project (using Lean)
Other proof assistants
Historical projects that died out:
Lean website (leanprover.github.io)
Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer, The Lean Theorem Prover (system description) (pdf)
Jeremy Avigad, Leonardo de Moura, Soonho Kong, Theorem Proving in Lean (pdf)
Robert Y. Lewis, Leonardo de Moura, Automation and Computation in the Lean Theorem Prover, contribution to HaTT 2016: Hammers for Type Theories, 2016 (pdf)
Thomas Hales, A Review of the Lean Theorem Prover, September 2018
Kevin Buzzard, Xena project (2018)
(on the Xena project)
Kyle Miller, Doing math the Lean way, Berkeley Lean Seminar (2020) [pdf, pdf]
Tutorials and workshops:
Lean for the Curious Mathematician 2020, online event (Jul 2020) [web]
Lean for the Curious Mathematician 2022, Brown University (Jul 2022) [web]
Lean for the Curious Mathematician 2023, Düsseldorf Univ. (Sep 2023) [web]
Last revised on June 13, 2025 at 22:25:44. See the history of this page for a list of all contributions to it.