Minimizing

One of the distinctive features of metamath is that the proofs are not only capable of being stored (rather than generated on the fly) but they are stored in a way that is human readable (for example can generate the web pages at metamath.org). Largely for this reason we care about proving things concisely, for a short proof requires less storage space, more clearly expresses which theorems it relies on, and (most of the time) is easier for a human to read because there is less to get through in order to understand it.

minimize_all

Although in theory we could have a wide variety of tools to make proofs shorter, in practice when people speak of "minimizing" a proof, they usually mean running the MINIMIZE_ALL command of the metamath-exe command line tool. We strongly encourage people to do this before submitting proofs (in the past there were centralized minimization runs but as set.mm has grown it has become less easy to set up a job to minimize every theorem in it).

Not everyone writes proofs the same way, so how to minimize this will depend on your own habits, but here are a few choices:

• If you are writing using metamath-exe's proof assistant, type minimize */allow */no_new ax-* after your IMPROVE ALL and before you save the proof.

• If you have written a proof and pasted it into a .mm file, from the command line you can run scripts/minimize THEOREM MM-FILE-NAME

• For global minimizations, there is scipts/minimize-all and scripts/min.cmd to minmize certain lists of theorems (those with given label-match, those within a given range, those using a given theorem... and many other variants) with other lists of theorems.

Manual minimization

Some kinds of minimization cannot be detected by current tools. For instance, no tool currently exists to identify builder theorems, which allow steps to be switched, effectively requiring a replacement of multiple steps with multiple steps, which of course cannot be done by current tools.

Commutations

Commutation theorems like "bicomi" may often be moved up builder theorems, then combined with a transitivity to save a step.

Here's a simple example. In step 2, bicomi is used. This commutation theorem is moved up (albii is a builder theorem) to step 3. There, it can be combined with bitri into bitr3i, saving a step.

original	lift bicomi

Here's a "random" theorem that uses bicomi. This time, we move bicomi 5 steps up so that it can be combined with 3eqtrd. As you can see, antecedent adding theorems also count as builder theorems.

(A better save is to move step 19 after step 10, adding a transitivity step and removing bicomi, step 20, 21, and 22; this saves three steps instead of one)

Antecedent adders

Builder theorems themselves may also be moved around. There are two mostly independent sets of builders: ones that remove antecedents, and ones that remove something from both sides of an equality or biconditional, which will be called consequent builders. (The latter generally must go in a specific order, while some antecedent builders can be switched with other antecedent builders. But more common is switching antecedent and consequent builders)

A metamath proof uses bytes to build a formula, so reducing symbols often reduces compressed proof bytes! To do this,

• we do the step that eliminates the most symbols as soon as possible, or
• if something can be eliminated before a conclusion is split into two or more hypotheses like oveq12d, then it's better to do that once before the split rather than twice after the split

Most consequent builders remove 2 constant symbols from each side of an equality or biconditional, plus 2 times however many variable/class symbols are removed; antecedent builders may generally remove little to humongous amounts of symbols.

As an exercise, try to find the minimization here:

answers

(None of the text above exactly describe either manual minimization I found ;)

• a1i can be moved after syl5rbb (which changes to bitr2i) where as a bonus it can be combined with bitrd
• Replacing ax-mp with mp1i and using some 3bitr* instead of bitrd would also technically shorten the proof, though it's obviously a worse option.