OpenAI withdrew three of its own mathematics results over a sign error
OpenAI’s mathematics repository, which publishes results produced with an internal frontier model and Lean proof formalisations, logged three withdrawals this week: “Algebraicity of Weil classes on split abelian eightfolds” and the two papers that depend on it, on Kuga–Satake correspondences and the rational Hodge conjecture for products of K3 surfaces. The stated cause is a sign error that “invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers.”
The same update revised fourteen other manuscripts — repaired crossing, boundary and convergence arguments, corrected statements and hypotheses — and added six more formalisations, bringing the share of top-line results formally verified to 300 of 719, about 42%. It lands the same week as a preprint arguing that OpenAI’s Lean-checked Navier–Stokes proof does not correspond to the natural-language argument it claims to certify.
WHY IT MATTERS
This is the second half of a point the week has been making from two directions: a machine-checked proof guarantees that the proof is valid, not that it proves what a press release says it proves, and a sign error in one lemma can quietly invalidate the papers built on top of it. The corrective behavior is real and worth crediting — the repository caught and disclosed its own error, and 42% formal coverage is a genuine audit trail most results never have. For a reader weighing any “our model proved” claim, the lesson is to ask what was formalised, against which statement, and what still rests on prose. The caveat deserves one line: the notice is OpenAI’s own, and the 42% figure counts what the lab chose to formalise.