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]> 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]. > 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/CAFXXJSvvZy2MUeUoWf_79ECBGZQPzwEb9rxzJd77gJcWLkBVQw%40mail.gmail.com.
