Week 5: Proof assistants

The tools a student proves with — mmj2, metamath-lamp, Yamma, mmt1, metamath-exe's own assistant — and how they differ from the verifier you will write.

22 March 2027

A proof assistant helps you build a proof; a verifier only checks one. The Metamath home page draws the line: “Proof assistants help you interactively create proofs”, while “Metamath verifiers do not make logical inferences; they just verify that the proof as stated is correct.” This week sets the verifier project: what you write will read the proofs these tools produce.

mmj2 is the assistant the labs use. Its README says it “includes a GUI for creating proofs, proof verification tools, and grammatical/syntax analysis”, that it “was originally developed by Mel O’Cat 2005-2011” and since “modified by Mario Carneiro and David A. Wheeler”, and that it needs Java. Its commands are in the Batch Command Documentation: LoadFile reads a database, Parse and VerifyProof check it, and RunProofAsstGUI opens the assistant. David A. Wheeler’s videos Introduction to Metamath & mmj2 (2014) and Walkthrough of the tutorial in mmj2 (2020) are listed on the site’s other topics page.

metamath-lamp, by Igor Ieskov, runs in the browser: its README says “users can use this proof assistant without installing anything”. The Metamath-lamp Guide “was primarily authored by David A. Wheeler”. Yamma is “A language server for .mmp files (metamath proof files)” inside Visual Studio Code, with unification and quick fixes for “missing disjoint vars statements” (README). mmt1 is “a mmj2 style proof assistant” with which “you can create not just metamath proofs, but also entire (grammatical) metamath databases” (README).

metamath-exe has an assistant of its own: “the PROVE command starts its proof assistant features; use HELP PROVE inside metamath-exe for further documentation” (other topics). The home page describes eimm as “An experimental proof export-import program” that “translates incomplete proofs in progress between the Metamath program’s CLI Proof Assistant and Mel O’Cat’s mmj2 GUI Proof Assistant”.

Three older tools, listed on the site in 2015: MM Tool, “a Metamath proof verifier and editor that runs in a browser (written in JavaScript by Ivan Kuckir)”; Igor, “A proof assistant for Metamath, specialized for set.mm (written in a custom language by Drahflow; in progress)”; and Milpgame, which takes a proof “either forward and backward relative to the statement to prove”.

Read#

• Introduction to Metamath & mmj2 — watch before Wednesday’s lab; it shows the worksheet you will work in.
• mmj2 Batch Command Documentation — the command file, and what VerifyProof does.
• Metamath-lamp Guide — the alternative if you cannot run Java; ask the tutor first.