Week 3 Lab: First proof

The first proving lab: build a short propositional-logic proof in mmj2's Proof Assistant, unify it, and see the verifier accept it. This lab counts toward the lab-proof mark.

10 March 2027

You prove one short theorem of propositional logic in mmj2 and leave with a worksheet the verifier accepts. From this week to week 11, each lab’s proof is marked as part of the lab-proof assessment.

Before the lab#

Do mmj2’s interactive tutorial, which its README says takes about an hour. The site’s Other Topics page lists two videos by David A. Wheeler that cover the same ground: an introduction to Metamath and mmj2 and a walkthrough of the tutorial. Check that your RunParms.txt still loads your set.mm; the LoadFile and RunProofAsstGUI lines are in the RunParm reference, and the home page’s Downloads section shows a working file.

In the lab#

The theorem is handed out on paper at the start: its hypotheses, if any, and its conclusion, in set.mm’s notation. Start mmj2, open the Proof Assistant, and build the proof as a worksheet, one step per line, each citing by label the hypotheses, axioms or earlier set.mm theorems it follows from. Ask mmj2 to unify; the README notes that the first unification can take several seconds and that it is quick after that. If it reports an error, fix the step and unify again. The tutor circulates; the point is not to be told the proof but to make the verifier stop objecting.

mmj2 does not write into a database. The README says that once a proof is complete you put it into a .mm file with another tool such as a text editor; later labs do that. Today the saved worksheet is the deliverable.

Afterwards#

Submit the worksheet file as the lab proofs page says, by 5pm on Friday; most people finish in the room and submit before they leave. It is marked on whether it unifies without error and whether every step cites a real label, and the mark and a line of feedback come back before the next lab.