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.
