> 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>
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].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/D406837B-B1E9-43D3-BA4E-D9B410F38D2A%40dwheeler.com.
