I also think that 200 is an okay "soft maximum". I've definitely got some theorems larger than that, some a lot larger, and the MM0 project is going to generate some really large proofs (the largest so far is 673 steps but that's still mostly handwritten; the autogenerated proofs are going to be huge), but given that several verifiers tend to choke on large proofs it's best to keep them out of set.mm.
On Mon, Dec 14, 2020 at 2:44 PM 'Alexander van der Vekens' via Metamath < [email protected]> wrote: > On Monday, December 14, 2020 at 7:30:30 PM UTC+1 David A. Wheeler wrote: > >> >> On Dec 14, 2020, at 12:52 AM, 'Alexander van der Vekens' via Metamath < >> [email protected]> wrote: >> >> Yes, I see - large proof would cause problems. In general, large proofs >> are problematic (difficult to understand/maintain, containing parts which >> could be useful as theorems by themselves, etc.). In my opinion proofs >> should usually not contain more than 100 (essential) steps, and maybe not >> more than 500 steps in extraordinary cases. Parts of large proofs should be >> extracted as separate theorems (if general enough) or as lemmata. But this >> is another topic to be discussed separately... >> >> >> >> The “conventions” text already hints at limiting size: >> >> <li><b>Organizing proofs.</b> >> Humans have trouble understanding long proofs. >> It is often preferable to break longer proofs into >> smaller parts (just as with traditional proofs). In Metamath >> this is done by creating separate proofs of the separate parts. >> A proof with the sole purpose of supporting a final proof is a >> lemma; the naming convention for a lemma is the final proof's name >> followed by "lem", and a number if there is more than one. E.g., >> ~ sbthlem1 is the first lemma for ~ sbth . Also, consider proving >> reusable results separately, so that others will be able to easily >> reuse that part of your work. >> </li> >> > > Thank you for this hint. > >> >> I would rather have long proofs than no proofs, so I think we shouldn’t >> make a hard-and-fast rule. >> 100 may be too small; perhaps recommend that they be under 200 instead? >> >> How about this revision (note I said 200 instead of 100, discussion >> welcome)?: >> >> <li><b>Limit proof size.</b> >> It is often preferable to break longer proofs into >> smaller parts, just as you would do with traditional proofs. >> One reason is that humans have trouble understanding long proofs. >> Another reason is that it’s generally best to prove reusable >> results separately, >> so that others will be able to easily reuse that part of your work. >> Finally, the “minimize” routine can take much longer with very >> long proofs. >> We encourage proofs to be no more than 200 essential steps, and >> generally no more than 500 essential steps, though these are >> simply guidelines and >> not hard-and-fast rules. >> In Metamath this is done by creating separate proofs of the >> separate parts. >> A proof with the sole purpose of supporting a final proof is a >> lemma; the naming convention for a lemma is the final proof's name >> followed by "lem", and a number if there is more than one. E.g., >> ~ sbthlem1 is the first lemma for ~ sbth . >> </li> >> > I am fine with this revision, even with the encouraged maximum of 200 > steps. I think it is a good idea to provide concrete numbers (instead of > saying "proofs should not be large") as a guideline, not a strict rule. > >> >> Feel free to slot in different numbers as guidelines. I know some people >> with the most expertise >> often create long proofs (hi Mario!), so 100, 200, and/or 500 may be too >> small to be reasonable >> in some cases. >> But as long as we merely “encourage” smaller proofs as guidelines I think >> it’d be okay. >> >> --- David A. Wheeler >> > -- > 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/a0794916-43c7-4c91-8a25-2665c4e46a5an%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/a0794916-43c7-4c91-8a25-2665c4e46a5an%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/CAFXXJSt8EEfHb8L70maK%3DrM%2BwKq8nB%2BG9KyqX3_7u6bd8Jupqg%40mail.gmail.com.
