I'm just thinking of two things: * Adding one of the theorems in the list may change the score of the others: for instance, the recently added theorem corresponding to 93 2 ["toponunii","restid","ax-mp","eqcomi"] probably changes the score of 124 2 ["restid","ax-mp","eqcomi"] which may not make it in the updated list anymore. Maybe between these two, it would have been better to add only the latter, instead of only the former.
* As you said, there should still be some pondering before adding a theorem, even with a high score. 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. It's not necessarily bad, and there's always a balance to find. Actually, I would generally prefer more reused lemmas, making for an often clearer proof, over a shorter but more cryptic proof. I guess this has similarities with using a high-level language versus completely optimized but obscure assembly code. Benoît On Saturday, July 9, 2022 at 9:50:50 AM UTC+2 Alexander van der Vekens wrote: > To have the number of essential hypotheses available is very useful and > interesting. I will have a closer look at the items no. 23, 27, 34/48 of > the list (they require no hypotheses and contain interesting combinations > of theorems). Unless the corresponding proofs look too awkward, and if they > really help to shorten proofs significantly, I will add them to set.mm > (together with the theorem corresponding to item no.6 which I mentioned > before, although it has many hypotheses - maybe this could serve as example > of the usefulness of such theorems). > > On Friday, July 8, 2022 at 8:00:24 PM UTC+2 savask wrote: > >> Here's the list supplemented with the number of essential hypotheses >> (second column): >> https://gist.github.com/savask/dce5b48b7317e8144635fda09e983fae There >> are quite a few theorems with 0-1 hypotheses even among the ones with long >> proofs, so maybe it's worth looking at these first. >> >> Jim Kingdon added theorem test4 to set.mm (thanks!), and as calculated >> by Alexander, a subsequent minimize_with run saved 2577 bytes. Theorem >> test4 was "inspired" by test3, which had score 93 in the table, so the >> savings were almost 30-fold of what was expected. >> > -- 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/45fd12c9-f3fd-497a-bad6-dde4d5cd9b20n%40googlegroups.com.
