Week 1: What Metamath is, and where it lives

Metamath in the project's own words: the language, the website and its mirrors, the licence, the GitHub organisation, and three unrelated projects that share the name.

22 February 2027

Open the slides

The project describes itself in one sentence: “Metamath is a simple and flexible computer-processable language that supports rigorously verifying, archiving, and presenting mathematical proofs” (Metamath Home Page). Everything in this course sits inside it. A database is a text file of axioms, theorems and proofs; a verifier checks every proof step in it. The name, the same page says, means “metavariable math”, and is not the branch of mathematics called metamathematics.

The website is served from two mirrors, us.metamath.org in the United States and cn.metamath.org in China, and the site asks that permanent links use the US one (Site Selection). The instructions for running a mirror are a short text file, and amount to a nightly rsync from the primary (mirror.txt).

The databases are public domain under CC0, with one exception, peano.mm, which is under the GNU GPL; the software on the site is GPL version 2 or later unless a file says otherwise (Copyright Terms). The same page dates the name’s public use from 1994.

Source code and databases live on GitHub. The metamath organisation holds the set.mm database, the metamath-exe program, the source of the Metamath book and the website sources (Home Page, “How can I contribute?”), but not everything: mmj2, the proof assistant used in this course’s labs, lives under a contributor’s own account at github.com/digama0/mmj2.

The Wikipedia article opens with a different sentence: “a formal language and an associated computer program (a proof assistant) for archiving and verifying mathematical proofs”, and it counts at least 19 verifiers for the format; week 3 returns to that count.

Three other things are called Metamath and are not this; a search for the course subject turns up all of them.

• A 2023 machine-learning paper on fine-tuning language models for mathematics, whose dataset is MetaMathQA (arXiv, as indexed by OpenAlex).
• A 2014 Russian-language article on a Tempus-programme project of that name in mathematics education (OpenAlex record).
• A 2026 paper titled “METAMATH: an ecological and innovating tool to assess mathematical metacognition in primary school” (OpenAlex record).

Read#

• Metamath Home Page: the Mini FAQ, from “What is Metamath?” to “Why is it called Metamath?”. Twenty minutes; the vocabulary for the whole course.
• Copyright Terms: short, and it tells you what you may do with what you download in Wednesday’s lab.
• Metamath on Wikipedia: a second description of the same thing, written by outsiders.