OpenAI has quietly withdrawn three of the 722 mathematical manuscripts it published after a sign error was discovered in one paper, according to a report from King's College London's student newspaper Roar. The withdrawal reduces the set to 719 papers. The manuscripts had been presented as a major output from a frontier model, including work on the Navier-Stokes existence and smoothness problem — one of the seven Clay Mathematics Institute Millennium Prize Problems.
Discrepancy between paper and proof code #
Researchers 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 one claimed in the natural-language version. In one lemma concerning 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 difference traces to different coefficient bounds in the Fourier-series estimates used in each version.
A second mismatch concerns 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, has different powers and factors of the radius, and is stated for every time in an interval rather than almost everywhere. The proof routes also differ: the paper uses boundedness of the Riesz transform on a particular function space and a specific cutoff factorisation; 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 authors of the alphaXiv analysis emphasise that these mismatches do not prove the natural-language theorem false. They show that the Lean formalisation does not faithfully correspond to the paper's argument. The Lean kernel checks only that the formal proof follows from the definitions and assumptions written in Lean; it cannot verify that those definitions and assumptions match the original mathematical text.
The sign error and the three withdrawals #
Separately, a sign error was found in another of the 722 papers. Roar reports that this error led OpenAI to withdraw that paper along with two dependent papers, bringing the total to 719. The sources do not specify who discovered the sign error.
Sebastian Janssen, president of the KCL Mathematics Society, told Roar that while an isolated error does not necessarily undermine the use of AI in mathematics, it does raise questions about the reliability of AI-generated arguments and the extent to which they require independent verification.
Mathematicians' broader concerns #
The episode comes amid mounting 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 off verification labour onto unpaid academics. The letter criticised AI-generated mathematics broadly; OpenAI withdrew its $1 million sponsorship of Caltech's student-run Mathathon in response. Anthropic kept its funding and has been working 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 the race 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 outright. Signatories acknowledge AI could accelerate genuine mathematical understanding if guided responsibly. What they object to is benchmark-chasing, rushed unattributed outputs, and the implicit claim that true/false verification is the same thing as mathematical progress.
The verification gap #
The Navier-Stokes case illustrates a structural issue. Lean formalisation is arguably the best-case scenario for agentic AI work: the specification is rigorous, machine-checkable, and audited. Yet even here, the translation from natural language to Lean can introduce mismatches that compilation alone does not catch. The alphaXiv paper proves that the problem of 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.
This means a compile-and-revise loop, where an AI revises a candidate proof until Lean accepts it, can repair a bad natural-language proof or replace a good one with a different argument. The resulting Lean code compiles, but the correspondence to the original reasoning is lost.
Competing narratives #
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. He described 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 — which is exactly what the mathematicians are asking for.
The gap between the labs and the community isn't really about whether AI can produce correct proofs. It's about what "solving" a problem means. For the labs, a verified proof is a solved problem. For mathematicians, a solved problem is one that has been understood, written up, reviewed, disseminated, and absorbed into the field's shared knowledge. Those are very different things, and conflating them is what's generating most of the friction.
What happens next #
The Navier-Stokes paper's natural-language claims have not yet been independently verified [1]. The alphaXiv authors recommend that researchers report two kinds of evidence separately: that the Lean proof checks, and that the formal statement and proof correspond to the source text.
Janssen suggests the future may not involve choosing between human minds and checking AI-generated work. "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." Whether the community accepts that redefinition of the mathematician's role remains an open question.
Sources #
1. [OpenAI claims progress on the Navier-Stokes Millennium Prize Problem](https://daily.dev/posts/openai-claims-progress-on-the-navier-stokes-millennium-prize-problem-jbi0dji6e) (daily.dev)
2. [Businesses in ChatGPT Terms](https://openai.com/policies/businesses-in-chatgpt-terms) (openai.com)
- Tentative AI Breakthroughs in Mathematics: the Philosophy of Mathematics - Roar News (roarnews.co.uk)
- Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs | alphaXiv (alphaxiv.org)