OpenAI's math proofs fall short of mathematicians' standards

When OpenAI released hundreds of claimed solutions to some of the world’s hardest math problems this week, the company said it had consulted an advisory group of elite mathematicians to avoid the kind of controversy that followed a previous case of one of its models solving a long-standing math problem. But OpenAI fell short of that group’s own standards, especially on ensuring humans actually understand the results — a concern sharpened by a new paper documenting gaps between the natural-language and formal versions of a solution to a million-dollar math problem that OpenAI’s models had ostensibly solved.

The Advisory Group on Mathematics and Artificial Intelligence (AGMAI), hosted by Princeton University’s Institute for Advanced Study and made up of nine prominent researchers from institutions worldwide, published guidelines for frontier AI labs solving math problems at the end of September. Responding to OpenAI’s latest proofs, AGMAI said it is ultimately up to the mathematical community to judge how well its recommendations were followed — though its first request was that labs stop testing advanced math problems on proprietary models, and OpenAI’s release explicitly says it evaluated proprietary models using open research problems.

OpenAI followed some of AGMAI’s principles, including releasing results quickly and explaining how the models reached their conclusions — but not all. Only 10 of the 719 manuscripts it released included the model’s chain of thought, and just 42% of its released proofs had been formalized, as AGMAI recommends for any proof people don’t understand. It remains unclear whether OpenAI is taking responsibility for ensuring human understanding follows, as AGMAI’s principles call for; the group suggested OpenAI help fund the mathematicians needed to make its solutions meaningful.

“Problems are being solved autonomously by AI prompters who have no interest in the broader field itself once their initial target is ‘solved’, and do not understand the AI output well enough to answer questions on the result, give talks, or otherwise interact with the rest of the field,” mathematician Terence Tao, a vocal critic of OpenAI’s approach, wrote on social media after the release.

That concern is underscored by a separate paper from mathematicians at Cambridge and King’s College London. AI models solving a math problem typically produce a natural-language explanation, then translate it into Lean, a programming language that in theory verifies a proof by compiling it as code. The paper finds at least two discrepancies between the natural-language proof and the Lean code behind OpenAI’s solution to a problem derived from the Navier-Stokes fluid-dynamics equations. The mismatches don’t necessarily disprove either version, the authors note, but they raise doubts about trusting models to formalize their own proofs without human review — a gap AGMAI tried to close by asking labs for metadata linking natural-language and formal proofs, which OpenAI didn’t provide.

Mathematicians say that when humans discover new results, they take responsibility for them, engaging the field through papers, talks, and seminars in ways that deepen understanding and open doors to new applications. Harvard mathematics professor Melanie Wood said that at the moment such results are released, there typically isn’t yet human understanding of them — meaning the real work only starts afterward.

Why it matters

OpenAI’s incomplete compliance with AGMAI’s guidelines raises the stakes for future AI-claimed proofs: how closely the mathematical community scrutinizes them now will determine whether such claims become verified contributions to the field or a recurring source of unverified, poorly understood results.