← Back to feed

One day after OpenAI released 722 mathematical manuscripts from an unreleased internal model, the company has updated its repository with a history file documenting withdrawals, proof repairs, and revisions. Three papers have been retracted. Fourteen others have been corrected. The total manuscript count now stands at 719.

The Cascading Failure

The root problem sits in a paper titled “Algebraicity of Weil classes on split abelian eightfolds.” OpenAI’s history log describes a sign error that “invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.” Because two other manuscripts were built on top of the flawed result, all three had to go.

The full withdrawal list:

• 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 third paper is notable. The rational Hodge conjecture for specific varieties — in this case products of K3 surfaces — is a significant goal in algebraic geometry, adjacent to one of the Millennium Prize Problems. The retracted version carried a notice explaining the gap and linking to the archived manuscript.

What Got Repaired

Beyond the three retractions, OpenAI revised 14 manuscripts with “proof repairs, corrected statements, clearer hypotheses and dependencies.” The repair clusters break down by topic:

• Lipschitz heights and Ashkin–Teller currents (4 manuscripts): repaired crossing, boundary-attachment, conditioning, and convergence arguments.
• Kähler minimal model programs and abundance (6 manuscripts): expanded positivity and contraction arguments, clarified which results are used as inputs.
• Taming and hypersymplectic deformation (2 manuscripts): corrected a cone-equality claim, added a strict-inclusion example, removed an unnecessary dependency.
• Incompressible Box Transport and Finite Computation: revised torus-projection and common-clock estimates.
• Exact Birch–Swinnerton-Dyer Formula: removed an obsolete citation to a withdrawn supporting manuscript.

An additional 13 manuscripts received reference updates to cite the revised editions of companion papers.

The Formalization Count

OpenAI also added 6 new formal Lean proofs and 5 other additions covering supporting results. The current formalization rate: 300 of 719 top-line results have been formally verified, approximately 42%.

That 42% figure is the more substantive number to track. Lean formalization is the only mechanism that catches errors like the sign mistake above before they cascade. The model that generated these proofs is internal and unnamed. The gap between “AI wrote a proof” and “a proof is formally verified” remains the operative distinction for any mathematician deciding whether these results are usable.

What This Says About the Process

The release model OpenAI chose — 722 manuscripts dropped simultaneously — guarantees that dependency chains go unreviewed before publication. A traditional journal process would catch a sign error before two dependent papers were drafted. Here, the error existed in the repository for roughly 24 hours before the history file acknowledged it.

OpenAI’s own math advisory group, formed in September, had flagged quality-control processes as a concern. The retraction count after one day of public scrutiny is consistent with those concerns.