Week 4 Lab: Navigate and prove

Find a theorem in the Proof Explorer and read its proof step by step, then prove a propositional theorem of your own in mmj2 with set.mm loaded.

17 March 2027

Before the lab#

Have mmj2 running with set.mm loaded before you arrive: its README says it “takes a time to get started (circa 60 seconds on a slow machine loading the large database set.mm)”. If you skipped the interactive tutorial before week 3, do it now; the README says it “ought to take about an hour”.

In the lab#

The first half hour is reading. Open the Theorem List, find the theorem you were assigned in section 1.2, Propositional calculus, and read its proof table. The site’s FAQ gives the trick for reading one: “look at the little colored numbers in the Ref column. The steps with the largest numbers are usually the ones you want to look at first. The steps with smaller numbers are typically logic “glue” to tie them together.” For each essential step, write down which axiom or earlier theorem it applies and what was substituted for each variable.

The rest is proving. In mmj2, start a new proof worksheet for your second theorem, type its statement, and build the proof step by step, unifying as you go, until every step is justified and mmj2 reports no errors. The README warns that “The first unification can also take several seconds”; after that it is fast.

Afterwards#

Save the worksheet and submit it as the lab proofs page says. mmj2 “does not update Metamath .mm databases”, so your proof lives in the file you saved, not in set.mm. Next week’s lab stays in mmj2 and goes further into how it unifies.