nLab proof assistants and formalization projects -- list

proof assistants:

based on plain type theory/set theory:

• Metamath

• Mizar, NuPRL, Isabelle, HOL

based on dependent type theory/homotopy type theory:

• Rocq, Agda, Lean, Arend

based on cubical type theory:

• cubicaltt

• redtt

• yacctt

• RedPRL

• Cube

• Cubical Agda

  • library and demos

• Mikan (forked from Cubical Agda), the proof assistant underlying the 1lab project

based on modal type theory:

• Agda-flat: installation instructions

based on simplicial type theory:

• Rzk

For monoidal category theory:

• DisCoPy

For higher category theory:

• opetopic type theory

• Globular, homotopy.io

projects for formalization of mathematics with proof assistants:

• Archive of Formal Proofs (using Isabelle)

• ForMath project (using Rocq)

• MathScheme

• UniMath project (using Rocq and Agda)

• Xena project (using Lean)

Other proof assistants

• Andromeda

Historical projects that died out:

• The QED Project