Benoit, As a follow-up, our provers failed on both proofs over the weekend.
It was kind of expected for ~midexlem given its length and our current capabilities; For ~mideulem it's also understandable given that it is based on ~opphllem which is barely used elsewhere. In particular, if the proof search misses ~opphllem's exact statement, it is as if it had to prove it which is, similarly to ~midexlem, still beyond our reach in terms of number of steps... for now. I'll keep an eye on both! -stan On Sat, Mar 28, 2020 at 12:29 AM Benoit <[email protected]> wrote: > > 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. -- 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/CACZd_0wzj-kmcs0_9RasnR51yz9vH6uht%2BmfEvu1eSAjr1QkXQ%40mail.gmail.com.
