A day after publishing 722 mathematics manuscripts, OpenAI withdrew three of them. The entry in the repository’s history is dated October 7 and names the cause: a sign error.
One error, three papers
The error sits in “Algebraicity of Weil classes on split abelian eightfolds.” It invalidates a stabilization-trace cancellation argument, and with it the construction two dependent papers were built on. So three manuscripts are gone:
- Algebraicity of Weil classes on split abelian eightfolds
- Algebraicity of Kuga-Satake Correspondences for K3 Surfaces
- The rational Hodge conjecture for products of K3 surfaces
Those pages now carry a notice explaining the gap and a link to the archived manuscript. OpenAI also revised 14 other papers, from repaired proof steps to corrected statements to one obsolete citation, and 13 manuscripts got updated cross-references to the revised editions. Six more formalizations were added. That puts formalized top-line results at 300 of 719, around 42%.
The advisory group asked for something else
OpenAI consulted a panel before publishing: the Advisory Group on Mathematics and Artificial Intelligence, nine researchers hosted at Princeton’s Institute for Advanced Study. Their guidelines from late September open with a request to stop testing advanced mathematical problems on proprietary models. That is exactly what OpenAI’s release says it is doing.
Other points OpenAI did meet: publish quickly, say how the models got there. The next one goes thin. The model’s chain of thought is published for ten of the 719 manuscripts.
Two gaps between the prose and the Lean
Separately, mathematicians at Cambridge and King’s College London put out a paper that goes after the method. A model first writes a proof in natural language, then translates it into Lean, where the compiler is supposed to confirm correctness.
The paper documents at least two places where the prose proof and the Lean code diverge, in a solution to a problem derived from the Navier-Stokes equations. Neither version is disproved by that. But it does put the question on the table: can a model be left to formalize its own solution with no human in between?
Terence Tao, a long-standing critic of the approach, wrote after the release that problems are being solved autonomously by AI prompters with no interest in the broader field and no grasp of the output deep enough to answer questions about the result or give talks on it.
The Association for Human Mathematics calls for a walkout
A second group is blunter. In an October 7 statement, the Association for Human Mathematics writes that releasing over 700 files at once is not a demonstration of scholarship but a demonstration of power. It urges mathematicians to discontinue their work with OpenAI.
The withdrawal happening is the good news
A sign error that drags two dependent papers down with it is precisely what review is supposed to catch. That it was found and logged inside a day speaks for the public repository, and against the idea that any of this is unauditable.
The real problem is the number ten. If 709 of 719 manuscripts stand without a published chain of thought and 419 without formalization, the burden of making them understandable lands on people who were never asked. Both panels say the same thing at different volumes: solving isn’t the bottleneck, understanding afterwards is. It’s the same shift Anthropic describes this week about security bugs.