based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
based on cubical type theory:
1lab (cross-linked reference resource)
based on modal type theory:
based on simplicial type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Rocq)
UniMath project (using Rocq and Agda)
Xena project (using Lean)
Other proof assistants
Historical projects that died out:
Last revised on June 13, 2025 at 22:11:30. See the history of this page for a list of all contributions to it.