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.
