A math professor at the University of Pennsylvania produces a complex mathematical proof using OpenAI's GPT-o1-mini. However, the path to this result is anything but straightforward.
Robert Ghrist, Professor of Mathematics and Electrical and Systems Engineering, uses AI language models to develop a proof for a generalization of the bottleneck duality theorem. Ghrist describes the process as a mix of "outrageous optimism and frustration."
Ghrist first worked with well-known AI models like GPT-4, Claude-3.5, and Gemini-1.5-Pro. While these models can make assumptions and provide evidence, they consistently fail due to subtle errors, Ghrist says.
The breakthrough came with OpenAI's new GPT-o1-mini model. According to Ghrist, o1-mini analyzed a faulty proof, found the errors, and then generated an "entirely new, clever, correct proof," that was "more elegant than the human proof" in just 43 seconds.
OpenAI's o1 language models are optimized for logical tasks using chain-of-thought techniques. They outperform traditional language models on logic and planning benchmarks, but are still prone to error.
AI support: A mixed blessing
Ghrist notes that the result is "right on the boundary of what is and is not provable via LLMs," explaining that "mapping out the failure modes was critical."
Despite the success, Ghrist admits that "it would have been faster to do it all without AI." However, he feels working with the AI models resulted in a "much better" paper.
The AI helped with initial guesses, some proofs, and most applications. Ghrist's paper includes an appendix documenting the role of the AI models in producing the results.
Ghrist sees exploring the "corners of math latent space where proofs almost work" as the best way to probe the potential of future AI models. However, he emphasizes that AI models are still far from delivering truly profound mathematical results.
Human mathematician has the edge
Shortly after publication, mathematician Sridhar Ramesh points out on X that the proof of the main result is possible without AI support. He points to a theorem by Birkhoff that greatly simplifies the proof.
Ghrist admits that he didn't know about this approach and that it would make things a lot easier, stating: "Humans win…"
