A verifier runs a stack#

It reads a proof as a list of labels. Section 4.1.4 of the Metamath book is the whole rule.

The rule#

• A hypothesis label pushes its expression
• An assertion label matches its hypotheses to the stack top by substitution, pops them, pushes the result
• At the end, one entry remains: the statement proved
• Every substitution respects $d

Metamath book, section 4.1.4

Five verifiers gate set.mm#

• metamath.exe, C, Norman Megill
• checkmm, C++, Eric Schmidt
• smetamath-rs, Rust, Stefan O’Rear
• mmj2, Java, Mel L. O’Cat and Mario Carneiro
• mmverify.py, Python, Raph Levien

How are the databases verified?

The same page also says#

• The algorithm “fits in two pages in the Metamath book”
• The Rust verifier typically checks set.mm in under a second
• Every other database gets metamath-exe alone

How are the databases verified?

The machinery#

A GitHub Actions workflow, verifiers.yml, run on every push and pull request.

Each job downloads, builds and runs one verifier.

checkmm, up close#

• One .cpp file from its author’s repository
• Its header comment: every verifier would have to share a defect for an invalid theorem to get in
• It counts four verifiers; the prose page counts five

checkmm.cpp

Testing the testers: metamath-test#

Databases that should and should not pass, with drivers for six verifiers.

Without the failing cases, “if you replaced a verifier with the program “true” it would produce the same results”.

metamath-test README

Testing the testers: mm-verifier-tests#

Edge cases, each marked $( should verify $) or $( should error $).

The verifier project, set in week 5, is run against both suites.

mm-verifier-tests README

How many verifiers exist#

• The home page: “over a dozen”
• The Other Topics list runs from Haskell and Lua to Julia, Zig and Lean
• Wikipedia: at least 19

Home Page · Other Topics · Wikipedia

Before Wednesday’s lab#

1. Do mmj2’s interactive tutorial; its README says about an hour
2. Or the two videos: introduction, tutorial walkthrough
3. Check RunParms.txt still loads your set.mm: RunParm reference

Read before next week#

• How are the databases verified?: one page, the most important this week
• verifiers.yml: the workflow itself; find the five jobs
• metamath-test README: why a verifier’s tests need proofs that must fail