# nLab Metamath

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Idea

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)

proof assistants:

based on plain type theory/set theory:

projects for formalization of mathematics with proof assistants:

Historical projects that died out:

## References

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

Last revised on June 12, 2021 at 11:46:39. See the history of this page for a list of all contributions to it.