On the afternoon of October 7, OpenAI withdrew three of the 722 mathematics manuscripts it had published the day before. The failure was a sign error in a proof concerning Weil classes — the sort of thing a first-year graduate student is trained to hunt for — and it did not stay put. The mistake propagated into the two papers that leaned on it, including a claimed result on the rational Hodge conjecture for products of K3 surfaces. Fourteen further manuscripts received proof repairs. Six new Lean formalizations went up. The catalog now stands at 719.

Every obituary for AI-does-mathematics wrote itself within about four hours. That is the wrong read, and it is the read that will look silly by spring.

A Public Changelog Is a Moat Nobody Else Is Building

State what actually happened. A lab posted several hundred proofs at once, someone found an error, and the lab publicly logged the error inside a day — by name, by dependency, with the count of remaining repairs attached to the same document.

Compare that with the human baseline. Mathematics retractions routinely take two to five years from first suspicion to formal notice, and the notice usually arrives as an unsigned paragraph in a journal that maybe nine people read. The withdrawn manuscripts here were flagged, counted, and de-listed inside a single news cycle.

I do not want to over-praise this. The changelog does not name who caught the sign error. Sit with that. Somebody — a postdoc, a contractor, an internal reviewer with a free weekend — did the single most valuable piece of work in this entire release, and the document recording it is anonymous.

One postdoc who spent part of that weekend checking the Weil-classes argument described the experience in a departmental Slack channel on Monday, in a message passed along to me: “The error is in the fourth line and it is not subtle. What is subtle is that nobody had a reason to look there.”

That is the sentence to keep.

The 419 Papers Nobody Can Check

Here is the number that should worry you more than three retractions: 42 percent.

After the repairs and the fresh certificates, roughly 300 of the 719 surviving manuscripts carry a machine-checkable Lean formalization. That leaves 419 papers — the clear majority of the release — asserting results with no certificate attached, across a range of problems the release barely bothers to sort, sitting on a public repository with a company logo on it.

Lean has earned its reputation as the industry shorthand for rigor. But a Lean certificate proves that the formal statement follows from the axioms. It does not prove the formal statement is the theorem the authors claim to have proven in English. That gap is exactly where a sign error lives comfortably for months, and where a chained dependency turns one bad line into three dead papers.

Meanwhile the company’s own framing, as given to The Atlantic this week, is that it expects mistakes to be “quite rare.” Rare relative to what? The model attempted roughly 3,600 additional problems, and none of those proofs were released. Nobody outside the building knows the denominator. When your error rate is quoted without a base, you are not reporting a rate; you are reporting a mood.

The comparison that should make OpenAI executives flinch landed on August 11, when Anthropic published a Claude research result raising the proven lower bound for Riemann zeta zeros on the critical line from 41.6 percent to 67.2 percent — with a public Lean formalization and named external reviewers attached. Same caveat about formal-versus-informal statements, better packaging. Verification has become a marketing channel, and right now a competitor with a smaller corpus is winning it.

Whoever Pays the Referees Sets the Standard

OpenAI has promised to pay mathematicians to study AI-produced results. The amount is unspecified. That is the entire ballgame, and it is being filed under housekeeping.

Institutions do not get to referee what they cannot fund. If verification money flows as grants from the lab that produced the proofs, the mathematics community receives a workforce without receiving independence — a consulting arrangement wearing a peer-review costume. If it flows instead through a body with standing to publish unflattering results and the budget to act on them, the field gets something it has never had: a real-time audit layer for a literature that now arrives in batches of seven hundred.

The sign error was never the story. The story is that OpenAI shipped a retraction mechanism alongside a product, and the retraction mechanism is the piece a rival would need years to copy. What remains undecided is whether the company funds that mechanism properly or keeps it as a press release — and whether the next person who catches a bad fourth line gets a name.

Three papers down. Four hundred nineteen unchecked. One anonymous reader who saved the field a year of citing a proof that was never true.

Sources