That's great, savask ! The list should be a good indicator of which lemmas to add. The number of essential hypotheses could modulate it, as you proposed. I'll try to have a look at them. Right now, I see a few which are within propositional calculus, which should probably be added (I think, 7 in the first 24). If you cut the list at the 24th, you have all the ones with score above 200, and all the ones with only two essential steps. It could be a good idea to look at these first.
As for the useless hypothesis in test3 versus test4, it is probably due to shared subproofs: the proof of test3 is shorter, and in proofs containing it as a subproof, what corresponds to the hypothesis test3.1 was already proved for another subproof anyway, so the proof could as well use it with no extra cost. Benoît On Wednesday, July 6, 2022 at 7:37:58 PM UTC+2 savask wrote: > >But is this a useful theorem? > > I personally don't think it is a very enlightening theorem, and I agree > with David's comment that items in the list should be considered only as > indicators of potential theorems. > > I'm not sure there's a way to tell if a theorem is interesting > automatically, but I can supplement the list with numbers of essential > hypotheses for each suggested lemma. That way things like > ["latjle12","syl13anc","mpbi2and"] with 9 essential hypotheses can be > avoided. > -- 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/405c724d-0a08-436f-a644-d491834000e7n%40googlegroups.com.
