Contents

Contents

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

proof assistants:

based on plain type theory/set theory:

based on cubical type theory:

based on modal type theory:

projects for formalization of mathematics with proof assistants:

Other proof assistants

Historical projects that died out:

References

Last revised on December 9, 2022 at 13:26:50. See the history of this page for a list of all contributions to it.