# nLab Lean

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