>As you said, there should still be some pondering before adding a theorem, even with a high score.
I think the main criterion should be whether the suggested theorem makes any mathematical sense. For example, no. 6 from the list doesn't make any sense to me, and it's definitely not a theorem which would come to my mind when formalizing a proof. Thus I would argue against adding it to set.mm even if it saves a few kilobytes of the database size, since it would hinder readability of set.mm proofs. On the other hand, test4 (now toponrestid in set.mm) looks like a reasonable lemma which was often re-proven over and over. Finding these kinds of lemmata is, I think, the ultimate goal. > A possibility is that a theorem appears in this list because a proof pattern occurs often. It could be that this proof pattern can be shortened in other ways, but if the theorem in the list is added, the resulting shortened proofs will not allow this kind of proof inspection. Of course it's not specific to the present list: the more lemmas are used in a proof, the more difficult a global minimization is. Perhaps a better solution then would be to run full minimize on affected theorems instead of minimize_with, so we can give metamath.exe a chance to shorten the proof in other ways before applying a new lemma? -- 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/b4b534fc-c9b3-41b2-8e67-6e0cba44aac8n%40googlegroups.com.
