OpenAI's Math Proofs Fall Short of the Field's Standards, Reviewers Say

OpenAI released 719 claimed solutions to open mathematical problems this week. Only 10 of those manuscripts included the model's chain of thought, the reasoning trace that might let a human understand how the AI reached its answer.

That gap sits at the heart of a widening fight between OpenAI and the mathematicians it hoped to please. The lab consulted the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), nine researchers at the Institute for Advanced Study, before going public.

What did OpenAI actually release?

The 719 manuscripts target open research problems in mathematics. OpenAI confirmed it evaluated its proprietary models on those problems. AGMAI had asked frontier labs, in guidelines published at the end of September, to "stop testing advanced mathematical problems on proprietary models."

OpenAI kept testing on its own models anyway. "It is ultimately up to the mathematical community to assess the extent to which our recommendations were followed successfully," AGMAI wrote in a statement on the release.

The lab did honor some of the principles. It shipped results fast. It included notes about how its models reached each conclusion. But on the harder parts of the framework, OpenAI fell short.

What standards are the mathematicians pushing for?

AGMAI's central worry is human understanding. A formal proof in Lean, the programming language that checks math as code, is not the same as a proof a person can defend, extend, or teach to a graduate student.

For papers where nobody can follow the reasoning, AGMAI recommended formalization. About 42 percent of OpenAI's 719 manuscripts, roughly 302 proofs, had not gone through that process at the point of release.

AGMAI also asked OpenAI to help fund the human mathematicians who would be required to make its solutions meaningful in any real sense. There is no sign that has happened.

Fields Medalist Terence Tao framed the deeper issue on social media after the release. He wrote that:

"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."

Tao sits at the top of the global math community. His criticism carries unusual weight, and OpenAI had hoped his advisory group's framework would defuse a repeat.

Why does this matter beyond OpenAI?

This is not a fight about one lab's products. It is a fight about whether AI proofs become part of mathematics at all, or stay research demos nobody can build on.

Harvard mathematician Melanie Wood told TechCrunch that human proofs come with an obligation baked in. "There is not human understanding of them at the point of release," she said, "and now the work begins."

When a human proves something, that person writes a paper. They give talks. They answer questions from peers for months. That loop turns a single result into a tool other mathematicians can reach for.

When an AI drops 719 proofs in a single announcement, the loop breaks. There is no author to email, no seminar to attend, no office hours to visit. The math community cannot engage, critique, or extend the work the way it has done for centuries.

What did the Cambridge paper find?

This week, researchers at the University of Cambridge and King's College London published a paper that puts a finger on the gap. They examined a proof OpenAI offered for a problem derived from the Navier-Stokes equations, which describe how fluids move.

When AI models solve math problems, they first write a natural-language explanation. Then they try to translate that explanation into Lean code, which the language compiles to confirm correctness.

The Cambridge team found at least two places where the natural-language proof and the Lean code did not match. The mismatches do not prove the underlying math is wrong. They show the model's translation can drift from its own stated reasoning.

"Because of the phenomenon of mistranslations — as highlighted in this paper — the NL proof by OpenAI and other autoformalised Lean proofs should not prima facie be trusted without the same peer review process and scrutiny that other proofs are subjected to," the authors wrote in their "lost in translation" paper.

AGMAI had asked OpenAI to include machine-readable metadata tying the natural-language parts of each proof to the formal parts. OpenAI did not include that metadata with this release.

So what happens next?

AGMAI declined to give a fuller written evaluation of the release. Its public statement passed final judgment back to the mathematical community. The Cambridge paper is the first peer-style review of the batch to surface publicly.

OpenAI now sits in an awkward spot. It promised to follow advisory standards before publishing. It chose which standards to honor. The standards it skipped are the ones that make proofs useful to anyone but the model that wrote them.

The next test is simple and unforgiving. If a mathematician outside OpenAI can pick up one of the 719 proofs, run the Lean code, follow the reasoning, and cite the result in their own paper, the release worked. If not, those 719 manuscripts will sit on the record as a demonstration run, and frontier labs will face the same questions every time they publish a batch of model-generated mathematics.