OpenAI withdrew 3 math papers over a sign error that cascaded

A single sign error in one model-generated proof invalidated two more that depended on it. OpenAI retracted three papers from its mathematical research release, recorded the pull in openai/math/history.md, and left archived versions in place with explanatory notices.

The withdrawn papers are "Algebraicity of Weil classes on split abelian eightfolds", "Algebraicity of Kuga-Satake Correspondences for K3 Surfaces", and "The rational Hodge conjecture for products of K3 surfaces". The repository notice says the first paper contained "a sign error [that] invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers". The two Kuga-Satake and K3 results relied on that construction and came out together.

What the same update changed

The same history.md entry records fourteen manuscripts revised with proof repairs and clarified dependencies, in four topic areas: Lipschitz heights and Ashkin-Teller currents, Kahler minimal model programs, taming and hypersymplectic deformation, and two further papers whose projection estimates and citations were updated. Thirteen more companion manuscripts were updated to reference the corrected versions. Six new formalizations and five supporting results were added to the Lean library.

The release the retraction applies to was announced as 722 manuscripts in 372 families, produced by one internal OpenAI model. OpenAI says the model was posed about 4,000 problems and averaged three hours of ChatGPT Pro thinking compute per result. The count on the repository is now 719 manuscripts, and OpenAI's own figure is 300 of them, 42 percent, formalized in Lean. The repository has 11,700 stars and an Apache 2.0 licence.

The Hacker News thread, and what commenters flagged

A Hacker News discussion on the retraction (item?id=50003107) collected 323 points and 311 comments at the time of writing. One line that recurs in the thread, and that the Latent Space roundup on the original release had already flagged, is that the proofs "are reported by individual commentators and have not been independently verified". Commenters also noted that the sign error was found by running a different LLM over the papers, so a verification pass before publication would have caught it.

The sign error ran through two more papers before it was caught

For a team shipping a product that chains model outputs, this is the same failure at smaller scale. Three papers were released together because two of them used results from the first, and the error in the first was not caught before the three went out together. The repair is the shape every eval-driven workflow describes: a check on each step before the step after it depends on the result, and a stored graph of which output builds on which, so a retraction can walk back every downstream artifact. OpenAI's history page lists the dependents it had to pull, which is the audit record arriving after publication rather than before.

The release also now carries a formalization figure that is OpenAI's own: 300 of 719 top-level results have been formalized in Lean. That subset has a machine-checked proof. The retraction is from the 419 results that do not.

Source

openai/math history.md, OpenAI · Hacker News discussion