constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Metamath is a proof assistant for creating databases of formally verified proofs. The proof language is extremely parsimonious using textual substitution as its only rule of inference (augmented by distinct variable constraints so that unfortunate variable captures can be prohibited).
One disadvantage of this philosophy is that definitions, syntax and axioms are all axioms. In particular, the user is responsible for ensuring that no ambiguities or contradictions are inadvertently introduced.
Metamath proof verifiers can be very small and simple, so many have been implemented in a wide variety of computer languages. Perhaps the most interesting was created by Stephen O’Rear using a language that makes Turing machines optimised for few states. This was used to reduce the bound of the smallest Busy Beaver Number that ZFC cannot prove to exist. A side effect was a small turing machine that halts iff the Riemann Hypothesis is False (and gives the smallest counterexample)
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq)
Xena project (using Lean)
Historical projects that died out:
Metamath was originally designed by Norman Megill, but many people have contributed over the years.
There are several Metamath databases on the Metamath website. The most developed covers classical ZFC set theory, but there is a very nice NF set theory database and a couple of other less well developed ones.
See also