OpenAI withdraws three math papers after sign error breaks central proof

What happened

OpenAI has withdrawn three mathematics papers from its research record after discovering that a single sign error undermined one of its central proofs. According to a changelog published in the openai/math repository on GitHub, which surfaced on the front page of Hacker News, the problem sits in "Algebraicity of Weil classes on split abelian eightfolds": an incorrect sign breaks a cancellation step in an argument involving stabilization traces, and the construction built on that argument was also load-bearing for two dependent manuscripts.

As a result, all three papers are gone from the active record: the Weil classes paper, "Algebraicity of Kuga–Satake Correspondences for K3 Surfaces," and "The rational Hodge conjecture for products of K3 surfaces." The changelog says the withdrawn manuscripts now carry notices describing the gap and linking to archived copies, and that earlier editions of revised papers remain available through version notes in their README files.

Fourteen more manuscripts repaired

The October 7, 2026 entry is not only about withdrawals. OpenAI also lists repairs to 14 other manuscripts, covering proof fixes, corrected statements, sharpened hypotheses and dependency clarifications, plus one obsolete citation that was removed.

The fixes span several areas:

• Lipschitz heights and Ashkin–Teller currents (4 manuscripts): crossing, boundary-attachment, conditioning and convergence arguments were repaired, along with additional work on the real-Lipschitz interface proof.
• Kähler minimal model programs and abundance (6 manuscripts): positivity and contraction arguments were expanded, and the papers now state more clearly which results they use as inputs and the hypotheses those inputs require.
• Taming and hypersymplectic deformation (2 manuscripts): a claim asserting equality of cones in "Taming implies compatibility" was corrected, a strict-inclusion example was added, and an unnecessary cone-comparison dependency was dropped from the hypersymplectic paper.
• Incompressible Box Transport and Finite Computation: the torus-projection and common-clock estimates were revised.
• Exact Birch–Swinnerton-Dyer Formula from Low Selmer Corank: an obsolete introductory citation to a removed supporting manuscript was deleted.

A further 13 manuscripts were updated purely so they cite the revised editions of companion papers, refreshing references and version dates.

Formalization continues

The changelog also records six new formalizations and five other additions covering supporting results. That brings the total share of top-line results that have been formalized to 300 out of 719, roughly 42 percent.

Why it matters

Retractions happen in mathematics, but a batch withdrawal driven by one character-level mistake is a stark illustration of how fragile long proof chains are. A sign error in one argument quietly invalidated two further results that depended on it, exactly the kind of cascade that formal verification tools are meant to catch. That makes the program's 42 percent formalization figure as interesting for what remains uncovered as for what is covered.

The event also bears on trust in AI-assisted research. The changelog does not say whether the proofs were produced by OpenAI's models, by human mathematicians, or some combination, nor does it explain how the error was found. What it does show is a lab treating its mathematical output as a versioned, auditable corpus: errors are documented publicly, withdrawn papers stay accessible in archived form, and dependent citations are traced and updated. That transparency is the more encouraging signal. For AI-assisted mathematics to earn trust, visible self-correction of this kind will likely need to become routine rather than newsworthy.