# nLab Archive of Formal Proofs

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Idea

The Archive of Formal Proofs (AFP) is an online library of formal proofs, examples, and projects formalized in the proof assistant Isabelle.

In contrast to other current projects, AFP and Isabelle are based on classical set theoretic foundations. It already comprises a large amount of concepts like smooth manifolds, Markov models, Monoidal Categories, or ordinals and cardinals to mention a few.

## References

Last revised on May 20, 2019 at 08:00:41. See the history of this page for a list of all contributions to it.