On Wednesday, February 15, 2023 at 8:56:36 PM UTC-5 wrote: "If anyone has thoughts about applying ML generative text models to Metamath proofs I'd love to hear them."
Hi David et al, I'm completing a CS PhD and my dissertation is on neural language models and automated/interactive theorem proving. I thought the mm community had already worked closely with OpenAI (see papers below) on GPT-f? We worked with them, but the work was their own, and there's no reason we can't do more :-). What I have in mind is a little different - using a large GPT directly. Also, I'm not worried if some of the answers are wrong; they wanted to see if it could generate *entire* proofs entirely automatically. I think it'd be perfectly reasonable to have a system that *tried* to create a proof, and even if it fails, provide some insight that would help a human create the proof. --- David A. Wheeler -- 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/1e6fa09d-eeec-4311-bda7-190cc0ac6aaan%40googlegroups.com.
