I hope you can run OpenAI on more proofs. Looking at some the first shortenings, it looks like it can behave as a more efficient "minimize_with" in some cases where there are many "weakenings". For instance, ~mideulem and ~midexlem use a lot of weakenings in the form of adantr, adantlr, ad2antrr, simplr, simprl... Could you run OpenAI on these two theorems to see what it does ?
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/b1bab644-ea9f-49ba-8238-0377228266ab%40googlegroups.com.
