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/a475a7a3-f807-402c-a2c8-baf952888b4e%40googlegroups.com.
