On Saturday, July 9, 2022 at 4:43:50 PM UTC+2 savask wrote: > On the other hand, test4 (now toponrestid in set.mm) looks like a > reasonable lemma which was often re-proven over and over. >
My first point above was about that particular example: now that the theorem corresponding to 93 2 ["toponunii","restid","ax-mp","eqcomi"] is in set.mm as "toponrestid", the score of 124 2 ["restid","ax-mp","eqcomi"] will probably drop and maybe it won't make it to your list anymore. Maybe it would have been better to add only the theorem corresponding to that former suproof, rather than only toponrestid. (Maybe both will still make it, I can't tell; my point is that if only one makes it, then maybe it should not be toponrestid but the other one.) > Perhaps a better solution then would be to run full minimize on affected > theorems instead of minimize_with, so we can give metamath.exe a chance to > shorten the proof in other ways before applying a new lemma? > Unfortunately, "minimize_with" only sees "obvious minimizations", and I was thinking of more global minimizations using different proof methods. I admit this is vague. All this is to say that, indeed, human inspection is important concerning potential new additions, as you wrote. Benoît -- 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/beff5dc7-ce9f-4d09-aa1e-dd3d91851c26n%40googlegroups.com.
