Week 3: Verification

What a verifier does, the five verifiers that check every change to set.mm and the workflow that runs them, the conformance suites, and how many more verifiers exist.

8 March 2027

Open the slides

A verifier reads a proof as a list of labels and runs a stack; section 4.1.4 of the Metamath book is the whole rule. A hypothesis label pushes its expression; an assertion label needs a substitution making its hypotheses match the top of the stack, which is popped, and pushes the substituted assertion; at the end one entry must remain, equal to the statement being proved, and every substitution must respect the $d restrictions. The home page: “Metamath verifiers do not make logical inferences; they just verify that the proof as stated is correct.”

That is why set.mm can afford five. Its verifiers page states that every change to set.mm and iset.mm is re-verified by five different verifiers: metamath.exe in C by Norman Megill, checkmm in C++ by Eric Schmidt, smetamath-rs in Rust by Stefan O’Rear, mmj2 in Java by Mel L. O’Cat and Mario Carneiro, and mmverify.py in Python by Raph Levien. The same page says the algorithm “fits in two pages in the Metamath book”, that the Rust verifier typically checks set.mm in under a second, and that every other database in the repository is verified by metamath-exe alone.

The machinery is a GitHub Actions workflow, verifiers.yml, run on every push and pull request; each job downloads, builds and runs one verifier. checkmm arrives as one .cpp file from its author’s repository, and its header comment makes the case for the arrangement: every verifier would have to share a defect for an invalid theorem to get in. It counts four where the prose page counts five.

Two test suites check verifiers themselves. metamath-test is a set of databases that should and should not pass, with drivers for six verifiers; without the failing cases, its README says, “if you replaced a verifier with the program “true” it would produce the same results”. mm-verifier-tests adds edge cases marked $( should verify $) or $( should error $). The verifier project, set in week 5, is run against both.

Far more verifiers exist than gate set.mm: the home page says “over a dozen”, the Other Topics list runs from Haskell and Lua to Julia, Zig and Lean, and Wikipedia says at least 19. When mmj2 accepts your proof on Wednesday, it has run the stack above.

Read

Teaching team