>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/5b4e8495-3fba-4632-b3e2-2716db11d9ddn%40googlegroups.com.
