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 can separate the relevant replacements from being done.

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 bitrd into bitr3i, saving a step.

original	lift bicomi

Here's a "random" theorem that uses bicomi. This time, we move the theorem 5 steps up so that it can be combined with 3eqtrd. As you can see, antecedent adding theorems also count as builder theorems. And of course, minimize_all cannot find this because the builder theorems act as opaque intermediates.

Antecedent additions

Theorems like a1i and adantr can also be moved up. When they are, a few more steps do not have an antecedent, so in effect the number of symbols are reduced! A metamath proof uses bytes to build a formula, so reducing symbols often reduces compressed proof bytes.

As an exercise, try to find the minimization here:

answers

a1i can be moved after syl5rbb (which changes to eqtr2i) where as a bonus it can be combined with bitrd

Another solution is to replace ax-mp with mp1i and use some 3bitr* instead of bitrd, though it costs a little bit to add the antecedent.