Week 9 Lab: 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.

5 May 2027

Before the lab#

Choose a target theorem that will not fit in one worksheet; Teodor has a list, or bring your own and ask on Monday. Write the plan before you open mmj2: the target as a Metamath statement, then each lemma as a Metamath statement with its hypotheses, in the order you expect to prove them, with the set.mm theorems you expect each to lean on. Look at how set.mm does it: the Metamath 100 page lists pnt with pnt2 and pnt3 beside it. A lemma is a statement, not a paragraph.

In the lab#

The first twenty minutes are plans. Teodor reads each one; a lemma whose statement is not well formed, or that quietly assumes the target, is rewritten before anything is proved.

Then prove the lemmas in order, one worksheet each. A lemma that will not go through is a plan problem before it is a proof problem: change the plan, write one line on why, and carry on. Put each finished proof into your database file with the editor as you go, since mmj2 “does not update Metamath .mm databases”.

In the last twenty minutes, verify the file. Run verify proof * in metamath-exe, which the Metamath book recommends doing periodically “to ensure their integrity.” Then run show trace_back <label> /essential /axioms on your target, the command Appendix 5 of the Proof Explorer home page gives for listing the axioms a proof depends on. The appendix also shows how to find where an unexpected one came in.

Afterwards#

The plan, with its changes, the database file, and the trace-back are this week’s lab proof submission. The plan is read as well as the proofs; a lemma that changed, with its line on why, counts for it.