I agree with the previous answers (Mario meant dfbi1ALT instead of dfbi1gb -- its label has been changed recently to conform to conventions).
I'll add that indeed, shorter metamath-proofs are very often easier to read and understand. When this is not the case, or when there are several genuinely different proofs, then it is a good idea to keep both (or more) proofs by using the xxxALT convention, as in dfbi1ALT. Benoît On Friday, March 27, 2020 at 9:06:17 PM UTC+1, Mario Carneiro wrote: > > I think the other posters have covered my thoughts on the matter already, > so I won't add much, but I did want to mention that regarding machine > learning to generate short proofs, I think it is extremely unlikely that > the proofs that are generated are going to be harder to understand than the > originals. The reason is because machine learning "thinks like a human" in > a number of respects; it learns heuristics and styles just like we do, even > when these heuristics are not absolutely optimal. You are much more likely > to find "bad short proofs" through exhaustive search or hard optimality > constraints, such as dfbi1gb. > > Mario > > On Fri, Mar 27, 2020 at 12:50 PM Richard Penner <[email protected] > <javascript:>> wrote: > >> On Friday, March 27, 2020 at 11:25:25 AM UTC-7, Marnix Klooster wrote: >>> >>> Hello all, >>> >>> Occasionally I see people here spending effort on making Metamath proofs >>> as short as possible. And every time I wonder, Why? >>> >>> >> From one point of view, "I just want to know what the theorems say" the >> shortness of the proof means little. But for the business of collecting a >> large number of proofs, having shorter proofs is a boon to those that have >> to store them, read them and understand them. Indeed, most proofs in the >> database can be expanded to thousands of steps by eliminating their >> dependence on proofs that came before, so emphasis on shortening proofs is >> practical even from the non-mathematical viewpoint of a curator. >> >> Shortening a proof means either a) one has eliminated wasteful steps by >> taking a more direct route, avoiding deriving the same statement twice, or >> using a step like "bicomi" (commuting a logical equivalence) more often >> than required or b) it means you proved the same statement with more >> powerful tools. And powerful tools are good things. >> >> Since Metamath builds up from the axioms, it starts a long way from the >> concepts that even children using math deal with on a daily basis ("2p2e4" >> is an example, since this concept of addition is powerful enough to work on >> negative, rational and complex numbers while the underlying set theory >> pieces don't speak immediately to such concepts). >> >> A recent example would be "intss" (If A is a subclass of B, then the >> intersection of class B is a subclass of the intersection of class A) which >> was shortened from a 10-step technical argument about the elements of A and >> B to a 5-step proof which points out that the subset relation of A and B >> gives rise to an implication of restricted quantifications, which gives >> rise to a subclass relation between classes of element which meet those >> restricted quantifications. When those classes are equated with the >> definition of the intersection of a class, we are done. >> >> The shorter proof is easier to translate. It's more symmetric in that it >> treats A and B identically. It's philosophically more concise in that it >> doesn't rely on the existence of a universal class of all sets. >> >> References: >> >> http://us.metamath.org/mpeuni/bicomi.html (logical equivalence commutes) >> http://us.metamath.org/mpeuni/2p2e4.html ( 2 + 2 = 4 ) >> http://us2.metamath.org:88/mpeuni/intssOLD.html (short lived link to >> proof from 1999) >> http://us2.metamath.org:88/mpeuni/intss.html (short lived link to proof >> from 2020) >> >> -- >> 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] <javascript:>. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/bb9250a2-60fc-45e2-bc37-1520bd6d60a7%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/bb9250a2-60fc-45e2-bc37-1520bd6d60a7%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- 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/a21d605a-fe20-4f88-bce0-d0c10727da30%40googlegroups.com.
