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.

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 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.