Labs
The twelve-week teaching schedule: what happens in each lab, what to prepare, and what leaves the room.
One lab a week, on Wednesdays, in the room with the tutor. Each page says what to have done before you arrive, what happens in the room, and what you hand in; the list at the end of each is what the lab requires, written so you can tell whether you have met it.
Install and verify
Get metamath-exe and mmj2 running on your own machine, download set.mm, and watch a verifier check every proof in it.
Week 1 · 24 February 2027
Read a small database, write a smaller one
Read miu.mm and peano.mm line by line, then write a database of about ten lines by hand and get a verifier to accept it.
Week 2 · 3 March 2027
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.
Week 3 · 10 March 2027
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.
Week 4 · 17 March 2027
mmj2 in depth
How mmj2 unifies a step, what a work variable is for, and how to grow a proof worksheet one step at a time until a theorem that needs several steps verifies.
Week 5 · 24 March 2027
Distinct variables
Prove a theorem whose proof needs a $d condition, then remove the condition and read the error the verifier reports.
Week 6 · 31 March 2027
A definition that fails
Add a definition to a copy of set.mm, run mmj2's definition check, watch it reject one, and fix it. The corrected definition starts your definition exercise.
Week 7 · 21 April 2027
Prove in iset.mm
The same theorem proved against set.mm and then iset.mm, to see where a classical proof needs excluded middle. Then the verifier project check-in: where your verifier should be by now.
Week 8 · 28 April 2027
A longer proof
Plan a proof that needs several lemmas before typing any of it, then prove the lemmas in order in mmj2 and verify the whole file in metamath-exe.
Week 9 · 5 May 2027
Read MM0 against Metamath
Read the Metamath Zero translation of set.mm's axioms beside the axioms themselves, line by line, and say what each file states that the other leaves out.
Week 10 · 12 May 2027
Verify a machine-found proof by hand
Take a short propositional proof found by exhaustive search, check every step on paper, then check it in mmj2 and with mmverify.py. The last lab that counts toward lab proofs.
Week 11 · 19 May 2027
Retrospective
Demonstrate your verifier on peano.mm and on a file you have not seen, then show one proof from the semester. The last lab; the verifier project is due this week.
Week 12 · 26 May 2027