The rules by which a proof is considered shorter were explained to me by Norm about 10 years ago: First look at the size of the encoding of the compressed proof, not taking the references into account. On tie, count the number of symbols used in the HTML display of the proof. I used the second rule extremely seldom in the past years, maybe twice or so. And I extended these rules by allowing one proof to be longer, if another/others benefit such, that in total their combined proof size shrinks. A recent example of this is neneqad. eqcom is an example that uses more definitions than the OLD one, and eqeq12i has the essential steps increased. All of these cases combined are rare, fewer than 5% I guess out of hand. Are shorter proofs less readable than others? IMO, certain techniques making twisted use of negation (like nsyl) force me occasionally to look/think twice. So, yes, from my personal perspective... it can happen. But not being able to grasp negated formulas that easily I consider my personal disadvantage. This is not really an objective argument As for the avoidance of definitions... well, what are they meant for, then? Is it really a good idea to expand them? And to take the idea further, theorems are again obstacles on the way to simplify proofs to just a sequence of axioms. I cannot quite follow here. But please, see and decide yourself whether the results mandate a change of rules. I gave you the examples above
Wolf Am Donnerstag, 28. November 2019 12:45:41 UTC+1 schrieb Benoit: > > A word of caution (without being dismissive whatsoever of Wolf's great > work): shorter proof (or, more precisely, proof with fewer steps) does not > always mean simpler proof, or easier-to-understand proof. This is why I am > thankful that Wolf keeps *OLD versions (which should be checked before > being deleted), and whenever the older proof has any interesting feature, > it should be kept as *ALT (or *ALT2, etc.). This may be the case (this is > not automatic) when: > - the longer proof (for the number of steps), actually has fewer essential > steps (I have seen a few cases, which unfortunately I do not remember), > - there is a tie, either in the number of steps or of essential steps, > - there exists a proof with fewer steps using more axioms (in which case > it is this one which should be the *ALT), > - the longer proof uses fewer definitions, or fewer syntax definitions > (more precisely: there exists a definition used by the shorter proof which > is not used by the longer proof), > - any other interesting feature, which makes the longer proof more > understandable, or have more structure, etc. (this part is obviously more > subjective). > > I lean to the side of having more alternate proofs rather than possibly > losing some information which might appear useful only in the future. I > also note that in the case of machine learning, having more alternate > proofs may also be an advantage. > > Benoît > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/45235cd7-5655-4f4d-8275-5721f9c25f73%40googlegroups.com.
