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/e9a12620-02b9-4be1-9896-ba6ff80a2b88n%40googlegroups.com.
