> On Dec 14, 2020, at 3:01 PM, Mario Carneiro <[email protected]> wrote: > 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 <http://set.mm/>.
No one’s going to be shot for exceeding 200. But if it’s really unusual for handwritten proofs to exceed 500, and the vast majority are under 200, then writing this down as a convention has succeeded. I would encourage even smaller proofs than that, especially if they create reusable proofs; I think there are hidden reusable gems in some of our larger proofs. If autogenerated proofs are huge, I presume it’s because they’re expanding something in place. That’s okay short-term. Longer-term, maybe we can modify the generators to also break up the proofs (e.g., if a template generates something long, create the template as a separate proof), or create a more-general proof that other proofs can directly use. So I think the guideline can help us create long-term improvements to generated proofs as well. *Verifiers* shouldn’t struggle with large proofs. Can you give an example? --- 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/900D5C2C-03CD-4D33-BFF9-2CA241ADA11A%40dwheeler.com.
