OpenAI has withdrawn three of the 722 AI math manuscripts it released a day earlier, according to the first changelog posted in its openai/math repository. The same update lists 14 revised papers and 13 citation updates, cutting the repository total from 722 to 719.
Three withdrawn papers were tied to the Hodge conjecture
The withdrawn manuscripts are all related to the Hodge conjecture, one of the Millennium Prize problems:
- 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
The problem began in the first paper. In its retraction note, OpenAI said a key argument wrote the sign of a geometric operation as +1, even though the paper’s own conventions required -1.
That single sign change altered the count used later in the proof. A quantity that should have canceled out to zero instead became nonzero. One classical theorem used by the paper required that count to be zero, so once that condition failed, the construction built on top of it no longer held. The other two papers borrowed the same construction and were withdrawn as a result.
OpenAI repeated the same point in all three retraction notices: the proofs were withdrawn, but that does not mean the mathematical statements themselves are false. The original drafts were not deleted and remain accessible through archive links.
Result family 032 has been renamed
All three papers belonged to result family 032, which had drawn attention earlier because of its connection to the Hodge conjecture. After the retractions, the family name changed from “Hodge and Kuga-Satake results for all projective K3 surfaces” to “The rational Hodge conjecture for CM abelian varieties.”
In practice, the K3-surface portion has been removed from the list. The family’s core claim, a proof of the rational Hodge conjecture for all complex CM abelian varieties, remains in place, and the new version of that paper only updates citations.
The paper that contained the sign error was dated Sept. 18, making it one of the earliest manuscripts in the repository. Nearly three weeks passed between that date and public release, and the paper was withdrawn within one or two days after publication. OpenAI did not say who found the error.
Fourteen more papers were revised
Beyond the retractions, OpenAI revised 14 manuscripts. The changes included patching proofs, correcting how conclusions were stated, and clarifying assumptions and dependency chains.
Those 14 papers span several areas: four in statistical physics on Lipschitz height and the Ashkin-Teller model, six in complex geometry on the Kähler minimal model program and abundance, two in symplectic geometry, one on universal computation in Navier-Stokes fluids, and one BSD formula paper that removed outdated references.
One representative revision appeared in result family 342, which claimed a proof of Simon Donaldson’s “tame implies compatible” conjecture. The main result did not change and has Lean formalization. But a stronger side claim in the paper was found to be overstated. The revised version narrows that statement to a specific case and adds an example showing it does not hold in general.
OpenAI says 300 main results are now formalized
The update also added six Lean formalizations and five auxiliary result supplements. By OpenAI’s count, 300 manuscripts now have their main results formally verified, or about 42% of the 719 papers in the repository.
Among the newly formalized items is result family 103 in theoretical computer science, which claims that log-space computation can be fully derandomized, stated as L = RL = BPL.
The report also noted that an earlier “about 60%” figure had been calculated by result family, meaning a family counted as formalized if even one paper in it included formalization. OpenAI’s 42% figure is based on individual papers’ main results, which gives a closer picture of how much has actually been checked line by line by a computer.
Most withdrawals and substantive revisions were in non-Lean sections
A comparison with the repository index shows a pattern: the withdrawn papers and the manuscripts that saw substantive revisions were concentrated almost entirely in parts without Lean formalization.
That lines up with earlier warnings from the mathematics community that results without formal verification and peer review should still be treated as claims.
OpenAI’s correction process, as described in the report, documented the error, spelled out the dependency chain, and kept older versions available for inspection. The article said that approach matches the “traceable revision” principle recommended by the Institute for Advanced Study’s mathematics and AI advisory group.
Still, the first correction sheet arrived only two days after more than 700 manuscripts were made public. As the original report put it, it is unlikely to be the last one.
OpenAI’s changelog is available here: https://github.com/openai/math/blob/main/history.md.