OpenAI Pulls Three Papers From 722-Manuscript Math Release

OpenAI has withdrawn three of the 722 mathematical manuscripts it published after researchers found a sign error in one paper, cutting the release to 719, according to King's College London's student newspaper Roar. The withdrawn set had been presented as a flagship output of a frontier model, including work on the Navier-Stokes existence and smoothness problem — one of the seven Clay Mathematics Institute Millennium Prize Problems. Who discovered the sign error remains unspecified.

What did researchers actually find?

A team from King's College London and the University of Cambridge found that the Lean formalisation of the Navier-Stokes paper establishes a weaker result than the paper's natural-language text claims. In one lemma covering an inverse estimate on the two-dimensional torus, the paper states that controlling a given number of output derivatives requires four additional input derivatives; the corresponding Lean declaration requires five. The gap traces to different coefficient bounds in the Fourier-series estimates.

A second mismatch involves a pressure-flux bound used in a velocity-uniqueness argument. The natural-language statement uses a localised velocity quantity, while the Lean theorem also depends on a localised gradient quantity, carries different powers and factors of the radius, and holds for every time in an interval rather than almost everywhere. The proof routes diverge too: the paper leans on boundedness of the Riesz transform on a particular function space and a specific cutoff factorisation, while the Lean proof uses a different cutoff decomposition, different Hölder exponents, an embedding into a space with sixth-power integrability, and boundedness of the Riesz transforms on the square-integrable space.

The alphaXiv analysts stress these mismatches do not prove the natural-language theorem false. They prove only that the formalisation does not faithfully correspond to the paper's argument. The Lean kernel checks that a proof follows from the definitions and assumptions written in Lean; it cannot verify that those definitions match the original mathematical text.

Why the verification gap is structural

The alphaXiv paper shows that resolving ambiguities in mathematical natural language to produce a semantically faithful translation is arbitrarily high in the Solvability Complexity Index hierarchy — informally, harder than the Halting problem. That has a hard consequence: a compile-and-revise loop, where an AI reworks a candidate proof until Lean accepts it, can repair a bad proof or silently replace a good one with a different argument. The code compiles; the correspondence to the original reasoning is lost.

Lean formalisation is arguably the best case for agentic AI mathematics — rigorous, machine-checkable, audited. If translation failures surface even here, weaker pipelines have thinner defences.

How are mathematicians responding?

The episode lands amid open friction between AI labs and the mathematical community. In late October, 771 mathematicians signed an open letter calling AI-generated outputs "slop mathematics" and accusing companies of offloading verification labour onto unpaid academics. OpenAI withdrew its $1 million sponsorship of Caltech's student-run Mathathon in response. Anthropic kept its funding and has worked directly with mathematicians, including using Claude to formalise Fermat's Last Theorem in Lean.

Twenty-five Fields Medalists, including Terence Tao, signed a declaration warning that racing to solve famous problems as benchmarks is misaligned with what mathematics actually is. Their core argument: solving a problem is only a proxy for conceptual understanding, and a poor one when the solution bypasses peer review, attribution, and the slow human process of turning a proof into shared knowledge. Nearly five thousand mathematicians signed a related statement. The declaration does not reject AI; signatories accept AI could accelerate genuine understanding if guided responsibly, and object specifically to benchmark-chasing, rushed unattributed outputs, and the claim that true/false verification equals mathematical progress.

Sebastian Janssen, president of the KCL Mathematics Society, told Roar an isolated error does not necessarily undermine the use of AI in mathematics, but raises questions about the reliability of AI-generated arguments and how much independent verification they demand.

What happens next?

The Navier-Stokes paper's natural-language claims remain unverified. The alphaXiv authors recommend reporting two kinds of evidence separately: that the Lean proof checks, and that the formal statement and proof correspond to the source text.

Sam Altman told Salesforce's Mark Benioff that an internal model beyond the current Astra release can do things the world's best mathematicians cannot, describing a progression: GPT-5.5 at the level of an average math professor, 5.6 at the top one or two percentile, Astra a bit better, and the next internal model past all of that. The claim is hard to evaluate without seeing the work — exactly what the mathematicians are asking for.

Janssen suggests the discipline's future may not be choosing between human minds and checking AI output. "Moving into the future, (our purpose) may not be to solve the problems, but to come up with them and be able to verify solutions … the middle work is now essentially being offloaded," he told Roar. Whether the community accepts that redefinition of the mathematician's role is the open question.