# nLab Lean

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

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

projects for formalization of mathematics with proof assistants:

Historical projects that died out:

## References

Last revised on September 12, 2019 at 03:04:44. See the history of this page for a list of all contributions to it.