nLab
Lean

Idea

Lean is a proof assistant based on dependent type theory. Like Coq and Agda, it may be used to implement homotopy type theory.

Formalized mathematics

Some mathematics that has been formalized in Lean (in particular in the Xena project):

• basic synthetic mathematics homotopy theory (HoTT)

  • github.com/groupoid/lean

  • github.com/gebner/hott3

• spectral sequences

  • github.com/cmu-phil/Spectral

• perfectoid spaces

  • github.com/leanprover-community/lean-perfectoid-spaces

• schemes

  • The Stacks Project

Related concepts

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Coq, Agda, Lean, Arend

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Coq)

• MathScheme

• UniMath project (using Coq)

• Xena project (using Lean)

Historical projects that died out:

• The QED Project

References

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

• Floris van Doorn, The Lean Theorem Prover, 2015

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

  • Installing Lean and mathlib

  • Learning Lean

  • What does Lean already know?

  (on the Xena project)