This is great to hear! I think this is indeed the first proof published designed with assistance of our tool. Thanks for the shoutout in your comment \o/
-stan On Sat, Jul 18, 2020 at 10:39 AM Thierry Arnoux <[email protected]> wrote: > Hi all, > > This is to highlight that I've used Stan's OpenAI based assistant to prove ~ > gsummptres <http://us2.metamath.org:88/mpeuni/gsummptres.html>. > Once I had manually filled-in the initial (less-trivial) first step, I > found the tool's suggestions were quite good. > > Even though we usually don't include this kind of information, I've made a > note in the comments about the fact that I've used OpenAI's prover, as I > don't know if anyone else has published any other theorem proven with that > tool. > > BR, > _ > Thierry > > -- > 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/7bae784d-6ebe-b29e-d7db-3fa5f7144fc4%40gmx.net > <https://groups.google.com/d/msgid/metamath/7bae784d-6ebe-b29e-d7db-3fa5f7144fc4%40gmx.net?utm_medium=email&utm_source=footer> > . > -- 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_0x1vU5WrLZef0PX4aCECoK5NJSpCCte21vTevmCGcqxCw%40mail.gmail.com.
