OpenAI withdraws three math manuscripts after a sign error

OpenAI has withdrawn three manuscripts from its public mathematics catalogue. The history file, in the section headed October 7, 2026, says that in “Algebraicity of Weil classes on split abelian eightfolds” a sign error “invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.”

The file then says: “As a result, we have withdrawn the following three manuscripts:”

• 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

It adds that the withdrawn papers now carry notices explaining the gap and linking to the archived manuscripts. A sign error here means a plus where the argument needed a minus, or the reverse. OpenAI says that one wrong sign broke a cancellation step, and that two further manuscripts depended on the broken construction.

What else the history file records

The same section says: “We have revised 14 other manuscripts with proof repairs, corrected statements, clearer hypotheses and dependencies, and one correction to an obsolete citation.” The groups it names are Lipschitz heights and Ashkin-Teller currents (4 manuscripts), Kähler minimal model programs and abundance (6), taming and hypersymplectic deformation (2), “Incompressible Box Transport and Finite Computation,” and “Exact Birch-Swinnerton-Dyer Formula from Low Selmer Corank,” where an obsolete introductory citation to a removed supporting manuscript was removed.

It then says: “Also, as a consequence of these fixes we updated 13 additional manuscripts to cite the revised editions of companion papers. These changes update references and version dates.”

On new checks, it says: “We have added an additional 6 formalizations and 5 other additions covering supporting results. This brings the total percentage of top-line results formalized to 300 / 719 = ~42%.”

The README now says the catalogue contains 719 manuscripts organized into 372 families, and that the repository has about 42 percent of top-line results formalized. An earlier report described that README as it stood on 7 October, when it listed 722 manuscripts in 372 families. The manuscript count is now three lower. That matches the three withdrawals. The family count is still 372.

The README still names a separate exception to the usual procedure: what it calls a proof of the Hodge conjecture for CM abelian varieties. That title is not one of the three withdrawn manuscripts. The withdrawn Hodge paper is the one on products of K3 surfaces.

Who published the update

The commit “Update manuscripts and Lean formalizations” is by Dan Roberts ([email protected]) at 05:03 UTC on 8 October 2026. On X, where his profile calls him a scientist at OpenAI, Roberts wrote at 05:20 UTC: “We’ve updated our GitHub math repo with 6 new Lean formalizations, 19 modifications, and 3 withdrawals. The repo now has ~42% top-line results formalized.” The 300 of 719 count is in the history file, not in that post. His 19 modifications line up with the file’s 14 revised manuscripts plus 5 other additions. The 13 citation updates are a separate line in the file.

What a Lean check is, and what this withdrawal settles

Lean is a proof assistant. A formalization rewrites a claim so a program can check each step. A finished Lean proof is a machine-checked version of that claim. An unformalized write-up still depends on a person reading it. The README says some unformalized results could have issues. Three hundred of 719 is the history file’s share of top-line results that now have a formalization, which it writes as about 42 percent.

A withdrawal after a sign error is the correction process that file describes: name the gap, withdraw the three manuscripts that use the broken step, and leave notices pointing at the archived text. The other manuscripts stay. Some have a machine check. Some do not. The withdrawal shows the checking process catching one error. It does not grade the manuscripts that remain.