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/06858df3-2a26-4b3a-b149-0fc8949ad7c5n%40googlegroups.com.
