OpenAI's First Math Errata: Three Papers Outside the Lean Catalogue, and One Corollary the Lean Never Covered

On 7 October OpenAI added a file called history.md to the repository of 722 AI-written mathematics manuscripts it had released the day before. The first entry is short. In a paper called “Algebraicity of Weil classes on split abelian eightfolds,” it says, “a sign error invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.” Three manuscripts were withdrawn: that one, a paper on Kuga–Satake correspondences for K3 surfaces, and a paper claiming the rational Hodge conjecture for products of K3 surfaces.

Last week I split the release in three: formalized results with short statements in standard Mathlib terms, formalized results that rest on new definitions, and 560 papers with no Lean at all, which I called claims. The first errata are a small sample, but they are the first real test of that split, and they fit it with one wrinkle.

The minus sign

The withdrawal notice on the root paper is unusually specific. In the paper’s signed double-point convention, it says, write \(I(f_1) = -m\) with \(m > 0\). The proof assigned each reverse stabilization trace a sign of \(+1\) and so claimed that inserting \(m\) of them brings the count to zero. Once you account for the opposite orientations of the two branches of a standard cusp, each trace contributes \(-1\) instead, and the count is \(I_{\text{new}} = I(f_1) - m = -2m \neq 0\). The cancellation theorem the proof calls on next needs a count of exactly zero. Its hypothesis fails, and the notice calls the construction that follows “unsupported.”

The two other papers inherit the error. Their notices say each “relies on an adaptation of the flawed stabilization-trace construction” in the first, which leaves their main theorems “unproved.” That is how one sign took down three manuscripts. The model’s papers cite each other, so an error in a foundation propagates through the citation graph the way it would through a human research program. Retraction Watch reported Alex Townsend of Cornell as saying the cascade was not surprising, and quoted him saying OpenAI “should have announced the manuscripts that were lean verified first.”

All three notices end with the same sentence: “This withdrawal concerns the proof; it does not assert that the mathematical statement is false.” That is the right distinction to draw. A withdrawn proof says nothing, by itself, about whether the statement is true.

The mechanics of the correction are better than I expected. Each withdrawn paper keeps its directory, with a notice in place of the manuscript and a link to the archived original at the initial commit. Revised papers get a new dated edition and a version note pointing back to the old one. The pull request that made the change was opened late on 7 October, Pacific time, and merged about a minute and a half later. Its description adds one sentence I would have put on the front page: “Lean builds were not run for this synchronization.” Two small things in the record don’t line up. The notices say “Withdrawn on October 6, 2026,” while the history entry is headed 7 October. And nothing in the repository says who found the error. An OpenAI spokesperson told Retraction Watch the company identified the errors during an audit, without saying what the audit covered.

Where the corrections landed

The same update did more than withdraw three papers. history.md says OpenAI “revised 14 other manuscripts with proof repairs, corrected statements, clearer hypotheses and dependencies, and one correction to an obsolete citation,” and updated 13 more “to cite the revised editions of companion papers.” That makes 30 manuscripts touched, and each one can be checked against the release’s catalogue of formalized papers. That catalogue, lean/formalization.yaml, listed 162 papers at the initial commit.

I matched every new edition in the update to the edition it replaced and looked each one up in that catalogue. None of the three withdrawn papers is in it. Neither is any of the 13 citation updates. Of the 14 revisions, one is. One other revised paper, “Incompressible Box Transport and Finite Computation,” is not in the catalogue but is among the papers covered by one of the repository’s Lean scope pages, which formalizes part of it. Counted that way, two of the 30 had some Lean behind them.

The 30 manuscripts touched by the 7 October update, by Lean status Unit chart, one dot per manuscript. Withdrawn: 3 manuscripts, none in the formalization catalogue. Revised: 14 manuscripts, one in the formalization catalogue (Taming implies compatibility on four-manifolds). Citations updated: 13 manuscripts, none in the catalogue. In total 1 of 30 is in the catalogue. If the 30 had matched the release-wide share of 162 of 722 papers, about 22 percent, roughly 6.7 would have been. One more revised paper, Incompressible Box Transport, is partly covered by a Lean scope page without being in the catalogue. THE 7 OCTOBER UPDATE · 30 MANUSCRIPTS · OPENAI/MATH Withdrawn Revised Citations updated 3 · sign error, one chain 14 · repairs, restated claims 13 · cite revised editions Withdrawn, not in the catalogue — Weil classes on split abelian eightfolds Withdrawn, not in the catalogue — Kuga–Satake correspondences for K3 surfaces Withdrawn, not in the catalogue — rational Hodge conjecture for products of K3 surfaces Revised, in the formalization catalogue — Taming implies compatibility on four-manifolds 0 of 3 1 of 14 0 of 13 in the formalization catalogue not in the catalogue At the release-wide share (162 of 722, about 22%), about 6.7 of 30 would be in the catalogue. Catalogue: lean/formalization.yaml at the initial commit. Counts are my own, from the repository.
The first errata came almost entirely from the part of the release with no machine check. That may reflect where the errors are or where the audit looked; the repository doesn't say.

If the 30 manuscripts had been drawn at random from the release, about seven would be in the catalogue. One is. That is a weak test. Thirteen of the 30 are citation updates that follow from other fixes, the three withdrawals trace to one error, and OpenAI hasn’t said what the audit covered. Errata turn up where someone looks. But the direction is the one you’d expect. A sign slip in a counting argument is about the most mechanical error there is, and a kernel would have caught it if the argument had been formalized. The papers that had a kernel behind them were nearly absent from the list.

The one with Lean

The one exception is “Taming implies compatibility on four-manifolds,” dated 23 September. It claims a solution to Donaldson’s tamed-to-compatible question: if a symplectic form tames an almost complex structure on a closed four-manifold, some symplectic form is compatible with it. This is a formalized paper. The repository’s scope document for it says the Lean “establishes this for every closed connected smooth four-manifold,” and there is a Comparator challenge for the statement.

The 23 September edition also has a Corollary 1.2. It combines the main theorem with an earlier cone comparison by Li and Zhang to assert an equality between two cones of cohomology classes: the classes of taming forms equal the classes of compatible forms plus a subspace of anti-invariant classes. The 6 October edition replaces it with a new Theorem 1.2, which describes the compatible cone differently, and a narrower Corollary 1.3. The version note says the new edition “restricts the cone-sum equality” to a special case and “adds a four-torus example of strict inclusion.” history.md describes the change as having “corrected the cone-equality claim.”

What the Lean covered in the Taming paper, and where the correction landed Diagram of the 23 September edition of Taming implies compatibility on four-manifolds. Theorem 1.1, that a tamed almost complex structure on a closed four-manifold admits a compatible symplectic form, sits inside the scope of the Lean formalization and its Comparator challenge. Corollary 1.2, a cone-sum equality derived with Li and Zhang's cone comparison, sits outside the formalized scope. The 6 October edition replaced the corollary, restricted the equality to a special case and added a four-torus example where the inclusion is strict. The withdrawn papers, by contrast, were not in the formalization catalogue. TAMING IMPLIES COMPATIBILITY · 23 SEPTEMBER EDITION · LEAN SCOPE The paper Theorem 1.1 A tamed almost complex structure on a closed four-manifold admits a compatible symplectic form Corollary 1.2 Taming cone = compatible cone + anti-invariant classes (via Li and Zhang's cone comparison) Formalized Comparator challenge TamingCompatibility.lean Not formalized Corrected 6 October: equality restricted, four-torus example of strict inclusion added Scope from lean/docs/342.md; correction from the 6 October version note and history.md.
The checked theorem and the corrected claim sat in the same paper. Only one of them was inside the formal scope.

As far as the repository shows, the correction did not touch Theorem 1.1, which is the part the Lean covers. The claim that had to be corrected was a corollary one step away, derived by citing a published result, and outside the formal scope. That is the gap I described last week, in a concrete case. “Formalized paper” is a label on a document. What the kernel checks is narrower: for this paper, one statement. Everything else in the paper, including results that sound like simple consequences of the checked one, is ordinary mathematics and needs an ordinary reader.

Johan Commelin, who directs the Mathlib Initiative, made the general version of this point to Quanta on 9 October. Hedging that he had not confirmed it firsthand, he said some of the formalizations “[appear to] prove weaker statements than what’s claimed in the paper. Or only formalize parts of the result claimed on paper.” Quanta also reported that “a handful of the Lean statements had technical issues.” I found no report, in the repository or in coverage, that the Taming paper’s Lean statement is weaker than its main theorem. It is the second case Commelin describes, a paper whose formal part is a strict subset of what it claims.

How far “compiles” sits from “says the right thing”

The research literature this year has started putting numbers on the related problem one level down: a Lean statement that compiles but does not say what the informal theorem says. Two 2026 benchmarks report both a compile rate and a faithfulness rate for the same system.

Compile rate versus faithfulness in two 2026 autoformalization benchmarks Slope chart. In Zhang and colleagues' June 2026 study of 227 graduate-level statements, a tool-augmented GPT-5.2 agent compiles 87.2 percent of statements but is faithful on 57.7 percent. In ShadowBench, an August 2026 benchmark of 178 postgraduate to research-level problems, Claude Code with Opus 4.8 and Numina-Lean-Agent reaches a 61.8 percent compile rate and an 11.2 percent semantic-alignment pass rate. LEAN STATEMENTS · COMPILES VS FAITHFUL · TWO 2026 BENCHMARKS Compiles Faithful 87.2% compile — Zhang et al., arXiv:2606.31002, June 2026 57.7% faithful — Zhang et al., arXiv:2606.31002, June 2026 61.8% compile — Han et al., ShadowBench, arXiv:2608.29270, August 2026 11.2% SA-Pass — Han et al., ShadowBench, arXiv:2608.29270, August 2026 87.2% 61.8% 57.7% 11.2% GPT-5.2 agent 227 graduate statements Claude Code + Numina agent ShadowBench, 178 problems Share of statements
Two benchmarks, two systems, two different faithfulness tests, so the lines are not comparable with each other. Within each one, the compile rate overstates faithfulness, by about 30 points in one and about 50 in the other.

Ke Zhang and colleagues, in a June preprint, evaluated eight systems on 227 graduate-level statements. A tool-augmented GPT-5.2 agent “compiles 87.2% of statements but is faithful on 57.7%.” The size of the gap depended heavily on the system, from 1.3 points for one-shot Gemini-2.5-Pro to 29.5 for that agent. Lean feedback drove most of the agent’s gain in compiling, and “nearly half of that gain consists of outputs that fail the semantic criterion.” The tool that makes statements compile also makes it easier to produce ones that compile and are wrong. ShadowBench, from Hojae Han and colleagues in August, uses harder problems and a stricter test: a candidate statement passes only if it implies, and is implied by, a set of auxiliary “shadow” statements. Claude Code running Opus 4.8 with a Lean agent compiled 61.8% and passed 11.2%. A third preprint, from Theodore Meek and colleagues, catalogues the ways it goes wrong: “incomplete multi-part statements, added weakening hypotheses, and parameter restrictions,” all of which “kernel acceptance entirely obscures.”

These are benchmark statements, mostly textbook and graduate level. None of these numbers is a measured error rate for OpenAI’s repository. I’d be wary of anyone who converts them into one. What they establish is narrower. A compiled Lean statement is a claim about faithfulness, not evidence of it, and the distance between the two is large enough to measure.

A number that needs a unit

The update also changed a headline number. The revised README now says the repository has “~42% top-line results formalized,” and history.md gives the arithmetic as “300 / 719.” Quanta repeated it, writing that OpenAI is “claiming formal verification … for some 42% of the papers.” But the catalogue of formalized papers lists 173 papers after the update, 24% of 719, and 168 if you leave out five entries history.md describes as supporting results. The 300 counts something else, presumably results rather than papers, since a paper can carry several. The repository doesn’t define “top-line result,” and the review field in that catalogue still reads status: unchecked. I can’t tell from the repository whether either number is off. They appear to count different things, and only the catalogue counts papers.

What a correction is for

The program usually called the first ever published has a bug in it. In Ada Lovelace’s Note G of 1843, which lays out a calculation of Bernoulli numbers for Babbage’s Analytical Engine, operation 4 divides two variables the wrong way round. Run as printed, it produces \(-\tfrac{25621}{630}\) where the eighth Bernoulli number should be \(-\tfrac{1}{30}\). Babbage, writing in 1864, recalled offering to work out the algebra for that calculation himself, and that Lovelace “sent back to me for an amendment, having detected a grave mistake which I had made in the process.” The checking went both ways, and a slip got through anyway. Nobody would call that unusual. It is what careful work looks like before a machine checks every line.

By that standard OpenAI’s first errata are good practice. The notice is dated and specific, it separates the proof from the statement, the original stays archived, and the dependency chain is named. What the record doesn’t give is the denominator. Retraction Watch reports a spokesperson said roughly 50% of the results were released unconfirmed, but the record doesn’t say which papers the audit read, or which of the remaining 719 have been checked beyond the catalogue’s unchecked status. The next history.md entry will mean much more if it says what was checked as well as what was wrong. Until then, I’m keeping last week’s split, with one amendment the Taming paper earned: “formalized” describes a theorem, not a paper.

References

  1. OpenAI (2026). openai/math repository: history.md, README.md, CONTENTS.md, lean/formalization.yaml, lean/docs/342.md and 376.md, withdrawal notices and version notes. GitHub, initial commit 6 October 2026; update commit 301488868, 8 October 2026 05:03 UTC. The matching of the 27 new editions to prior editions and to the formalization catalogue, and the counts of 162 and 173 catalogued papers, are my own, from the repository as read on 15 October 2026.
  2. OpenAI (2026). History, entry headed 7 October 2026.
  3. OpenAI (2026). Withdrawal notice: Algebraicity of Weil classes on split abelian eightfolds. Notice dated 6 October 2026.
  4. OpenAI (2026). Update manuscripts and Lean formalizations, pull request #1, merged 8 October 2026 (UTC).
  5. OpenAI (2026). Taming implies compatibility on four-manifolds, 23 September 2026 edition, and revised edition with version note, 6 October 2026.
  6. Gallegos, A. (2026). OpenAI withdraws three preprints a day after releasing 722 manuscripts on unsolved math problems. Retraction Watch, 8 October 2026. Source of the Townsend remark and the spokesperson’s statements.
  7. Quanta Magazine (2026). Cracks appear in OpenAI’s wall of proofs. 9 October 2026. Source of the Commelin quote and the “42% of the papers” wording.
  8. Zhang, K., Gallardo Candela, P., Murthy, S., Xie, Y. et al. (2026). Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization. arXiv:2606.31002, 30 June 2026.
  9. Han, H., Kim, J., Park, S., Cheon, D. et al. (2026). SHADOWBENCH: Toward Reliable Automatic Evaluation of Semantic Alignment in Autoformalization. arXiv:2608.29270, 29 August 2026.
  10. Meek, T., Ge, S., Xiang, D. Q., Chess, S. et al. (2026). Formalizing Numerical Analysis: An Agent Pipeline and Quality Audit Beyond Kernel Acceptance. arXiv:2606.14000, 12 June 2026.
  11. Wikipedia (2026). Note G. Dated background: Lovelace’s 1843 note, the operation-4 division error, and Babbage’s 1864 recollection in Passages from the Life of a Philosopher; checked 15 October 2026.