In despite of large proofs being problematic. They are solutive. The question is if a large proof giver a better understanding then a short proof. Or can a big proof maintain more information. I believe that all bigger proofs van be written as small proofs. There is where I might go wrong. Instead larger proof can maintain more information. So they are uniqe and give more information. That itself is a fact. But what’s the truth about it.
Verzonden vanuit Mail<https://go.microsoft.com/fwlink/?LinkId=550986> voor Windows 10 Van: [email protected] <[email protected]> namens David A. Wheeler <[email protected]> Verzonden: Monday, December 14, 2020 7:30:22 PM Aan: Metamath Mailing List <[email protected]> Onderwerp: [Metamath] Recommending proof length limits On Dec 14, 2020, at 12:52 AM, 'Alexander van der Vekens' via Metamath <[email protected]<mailto:[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> 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> 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]<mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/D406837B-B1E9-43D3-BA4E-D9B410F38D2A%40dwheeler.com<https://groups.google.com/d/msgid/metamath/D406837B-B1E9-43D3-BA4E-D9B410F38D2A%40dwheeler.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/AM0PR08MB50604FA1DEE709A7B4EA888F83C60%40AM0PR08MB5060.eurprd08.prod.outlook.com.
