אִם יִרְצֶה הַשֵּׁם
On October 6, OpenAI withdrew three preprints from its new openai/math corpus: 372 result families, 722 manuscripts, a genuinely ambitious attempt at machine-produced mathematics. The headline casualty was "Algebraicity of Weil classes on split abelian eightfolds." The killer: a sign error in the stabilization-trace argument. Two dependent papers (Kuga–Satake for K3 surfaces, rational Hodge for products of K3) went down with it. Fourteen more manuscripts were quietly revised the same day.
The error
Let me be precise about what this error was, because it's beautiful in the way only a fatal triviality can be. The paper inserted "reverse stabilization traces" into a cobordism and claimed each contributed +1 to a signed double-point count, canceling −m existing negative double points to reach zero: the exact hypothesis needed to invoke Eliashberg–Murphy's cancellation theorem. Except the paper assigned its traces the sign of the wrong geometric object. The traces run from a more-stabilized link to a less-stabilized one: the destabilization direction. In the paper's own cited authority (Ekholm–Eliashberg–Murphy–Smith, Lemma 3.4 proof), that direction is the G₃ trace, with double-point sign (−1)^{k−1}. The paper instead used (−1)^k, the sign of G₂, the lift of the inverse stabilization homotopy. Same direction, different homotopy, opposite sign. At k=4: each trace contributes −1, not +1. The replayed count is −2m, not 0. The cancellation hypothesis fails on the paper's own terms.
The machine
I know this because I built a machine that replays exactly this kind of argument. And I want to be honest about timing: we ran our own reconnaissance of the openai/math corpus on October 7 (parsed the full catalog cell by cell, matched their advertised totals exactly) and built the Weil-sign gate after the withdrawal, deliberately without reading the withdrawal notice, as a calibration test. We did not find this error before OpenAI pulled the papers. What we showed is that a dumb, mechanical replay of the paper's own text against the paper's own cited reference flags the contradiction without any human mathematical insight.
Here's what the harness does. The fragile-proof-audit campaign runs 32 verification gates over published claims: 17 BREAK, 15 PASS. A gate takes the paper's own stated steps, recomputes them mechanically, and checks whether the paper's conclusions follow from the paper's own premises. Lean 4 formalizations must be sorry-free and kernel-checked; hardened axiom audits permit only propext, Classical.choice, and Quot.sound, which, notably, is exactly the axiom list OpenAI's own comparator challenges for Catalan require, so the tooling applies directly. And every gate answers a statement-fidelity checklist (does the formal statement match the claimed theorem, does the argument correspond, is the credit honest), because, as a recent arXiv note observes, Lean acceptance certifies the formal object, not its correspondence to the natural-language claim.
The gap is coverage
OpenAI does have verification: comparator challenges, permitted-axiom lists. I'm not going to pretend they ship nothing. The gap is coverage. In our recon: 235 of 372 families have Lean scope docs; 162 cataloged formalizations across 127 families; but 137 families have no Lean doc at all: pure-manuscript claims, unauditable by machine. All three withdrawn papers sat in the unconfirmed ~58%. A sign error walked straight through the manuscript-only majority and was caught, presumably, by a human reader: the most expensive and least scalable detector known to mathematics.
"Given the skepticism of AI in the mathematics community, I think that OpenAI should have announced the manuscripts that were lean verified first." — Alex Townsend (Cornell), quoted in Retraction Watch
There's a broader point our recon turned up, and I'll call it Gap C: some comparator challenges check a lemma while the scope note claims a theorem. A check that covers less than the claim is a coverage decline, not a verification. You can have a green checkmark and an unverified theorem in the same repo, and nothing in the pipeline will tell you.
The boring steps
The Weil-sign gate took the paper's PDF, pinned its hash, replayed the sign assignment, and returned BREAK with control NO FALSE POSITIVE: the replayed −2m matched the withdrawal notice exactly. Not because the machine is clever. Because sign conventions are the kind of thing that breaks mechanically and silently, and mechanical replay is the only detector that doesn't get tired, distracted, or impressed by the rest of the argument.
Machine-generated mathematics is going to produce errors like this at scale. The fix isn't better mathematicians. It's a harness that replays every claim from its own premises before publication: especially the boring steps, especially the sign conventions, especially the parts a human reviewer skims because the proof "obviously works."