OpenAI withdrew three mathematical proof manuscripts produced by an internal artificial intelligence model on October 7, 2026. A sign error undermined an argument in one manuscript and a construction used by two others. This is not evidence that the Lean proof checker failed. Lean can establish that a formal deduction follows from stated assumptions, but that check alone does not guarantee that the formal statement matches the mathematical problem researchers intended to solve or that the result is a new discovery.
From publication to corrections: the documented timeline
On October 6, OpenAI published 722 manuscripts grouped into 372 result families in the public openai/math repository. The company attributed the material to an unreleased internal model and described the papers as research outputs at different stages of verification. A preprint, in this context, is a paper made public ahead of conventional peer review, not a conclusive certification.
In its October 7 history entry, the company withdrew three papers, revised 14 other manuscripts with proof repairs and changes to hypotheses, statements or citations, and updated 13 more to cite corrected editions. The same entry reported six additional formalizations and said 300 top-line results out of 719 manuscripts were formalized in Lean, approximately 42%. This was OpenAI's published calculation at that date, not an independent audit of every file.
The catalog continued to change. On October 26, OpenAI added two manuscripts with accompanying formalizations; the README consulted on October 30 listed 721 manuscripts in 373 families. On October 29, the change history recorded a namespace correction between the Comparator challenge and solution for another result concerning CM abelian varieties. That change must not be confused with the October 7 withdrawals or with the withdrawn paper about products of K3 surfaces.
Which three manuscripts were withdrawn?
The official history identifies the papers by these original titles:
- 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 first manuscript contained a sign error that invalidated a cancellation argument involving stabilization traces. The other two relied on the affected construction. All three were therefore withdrawn, with notices describing the gap and linking to archived versions. This is a flaw in the argument as presented, not proof that the conjectures themselves are false.
What does Lean actually verify?
Lean is a programming language and interactive formal proof assistant. Rather than accepting a natural-language explanation because it looks plausible, its checking kernel determines whether a proof object establishes a proposition expressed with precise definitions and logical rules. Lean's documentation distinguishes finding a proof from checking one: an AI system may propose reasoning, while the checker evaluates its formal representation.
That assurance is conditional on the formal statement, definitions, axioms and dependencies used. A theorem can be correctly proved in Lean yet address a narrower, different or poorly translated version of an informal mathematical claim. For example, establishing a property for a special class of objects does not prove it for all objects, even when the formal proof is flawless.
Lean's manual warns that an editor's success indicator is not enough for every audit: dependencies may contain sorry, a placeholder for missing proof steps that becomes an axiom. The #print axioms command helps inspect axioms and assumptions, including indirect dependencies. For stronger verification, lean4checker and comparator provide additional checks; Comparator matches the proved theorem against a trusted challenge statement. Even that procedure relies on the correctness of the challenge and its definitions.
Three questions that should not be conflated
| Layer | What is examined | Crucial limitation |
|---|---|---|
| Logical validity | Does the formal proof follow from its stated definitions, axioms and premises? | Technical checking does not automatically repair a poorly stated theorem. |
| Statement fidelity | Does the encoded proposition faithfully express the original conjecture without weakening it? | Requires mathematical examination of the meaning of definitions and assumptions. |
| Scientific contribution | Is the result novel, relevant, understandable, properly credited and supported by scholarly scrutiny? | Requires literature review, independent criticism and scientific discussion; successful compilation alone is insufficient. |
What mathematicians said and why the caveats matter
In an October 8 report, Retraction Watch reported that an OpenAI spokesperson said the error had been found during the company's own audit. Alex Townsend of Cornell University argued that already formalized papers should have been released separately from the others. Andrew Sutherland of MIT considered the swift withdrawals appropriate but stressed that rebuilding trust would take more work. These are attributed assessments by the researchers, not a universal verdict from the mathematical community.
In recommendations published on September 29, 2026, the independent AGMAI advisory group called for transparency about the model, prompts, attempted problems, computational costs, formalization artifacts and which papers had not yet been verified. It also emphasized human understanding, peer review where appropriate, and preserving records of revisions. Its guidance allows the release of work without complete formalization under transparency conditions; it does not turn release into scientific validation.
On October 26, OpenAI itself described AI-produced manuscripts as raw research data and announced different arrangements for collaborating with outside experts to explain new results. This procedural shift does not retroactively validate the three withdrawn papers.
What the episode does and does not establish
The documented conclusion is specific: three published arguments did not hold in the form released, and OpenAI corrected or updated other papers. That does not establish that the entire collection is invalid, that Lean approved those three proofs or that its checking kernel was defective. The documents consulted do not include independent execution by DTech of the formalizations or a comprehensive verification of every manuscript.
To assess any new AI-generated proof, readers need to know exactly which statement was formalized, whether axioms and dependencies were audited, how much of the reasoning was checked, who reviewed the match with the original conjecture and what scientific scrutiny followed. A logical proof check answers a vital question, but it does not replace the others.
Sources and references
- OpenAI, October 6 announcement
- OpenAI, repository and current catalog
- OpenAI, withdrawal and correction history
- Lean, formal proof validation manual
- Lean, introduction to theorem proving
- Retraction Watch, independent October 8 reporting
- AGMAI, September 29 recommendations
- OpenAI, October 26 collaboration approach
