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

References

Last revised on May 20, 2019 at 04:15:11. See the history of this page for a list of all contributions to it.