What Metamath is, and where it lives

SLOP3373 Metamath 101 · Week 1

Noor Castellane

The course

  • Lectures on Mondays
  • Labs on Wednesdays
  • From week 3, every lab ends with a proof in mmj2
  • From week 5, you write your own verifier, due at the end of week 12

“Metamath is a simple and flexible computer-processable language that supports rigorously verifying, archiving, and presenting mathematical proofs.”

— Metamath Home Page

Two words for the whole course

  • A database is a text file: axioms, theorems, proofs.
  • A verifier is a program that checks every proof in it.

Mini FAQ, “What is Metamath?”

The name

It means “metavariable math”. It is not metamathematics, the branch of mathematics that studies mathematics itself.

The name has been in public use since 1994.

Mini FAQ, “Why is it called Metamath?” · Copyright Terms

Where it lives

  • us.metamath.org — primary mirror, United States
  • cn.metamath.org — secondary mirror, China

Permanent links use us.metamath.org. So does your work.

Metamath Site Selection

How a mirror stays in step

rsync -vrltS -z --delete --delete-after --block-size=400 \
    rsync://rsync.metamath.org/metamath /var/www/html/metamathsite

A nightly cron job, pulling from the primary. The whole recipe is one text file: mirror.txt

The licence

  • Databases: public domain, under CC0
  • The exception: peano.mm, under the GNU GPL
  • Software on the site: GPL version 2 or later, unless a file says otherwise

Copyright Terms

On GitHub: the metamath organisation

  • set.mm, the database
  • metamath-exe, the original program
  • metamath-book, the specification’s source
  • the website’s seed files and scripts

github.com/metamath · Home Page, “How can I contribute?”

Not everything is there

mmj2, the proof assistant the labs use from week 3, lives under a contributor’s own account:

github.com/digama0/mmj2

A second description

Wikipedia: “a formal language and an associated computer program (a proof assistant) for archiving and verifying mathematical proofs”.

It counts at least 19 verifiers for the format.

Metamath on Wikipedia

Five verifiers, five languages

The Proof Explorer “is routinely checked by 5 independently-created verifiers in 5 different programming languages”.

Yours will be one more.

Mini FAQ, “How confident can I be in the proofs?”

Three other things are called Metamath.

None is this.

The other Metamaths

  • 2023: a language-model paper and its dataset MetaMathQA — arXiv, OpenAlex
  • 2014: a Russian-language article on a maths-education project — OpenAlex
  • 2026: a paper on assessing metacognition in primary school — OpenAlex

Before Wednesday’s lab

  1. metamath-exe: the portable executable, or compile the C source, as its README says
  2. mmj2: follow INSTALL.md in the repository; it needs Java
  3. set.mm: github.com/metamath/set.mm

Read before next week