On October 6, OpenAI posted 722 manuscripts to a public repository, claiming progress on 372 families of open math problems across geometry, algebra, and theoretical computer science. On October 7, the day after, three of them were withdrawn. The catalogue now reads 719.
The cause was small in the way these things usually are. A manuscript titled “Algebraicity of Weil classes on split abelian eightfolds” contained a sign error that invalidated a stabilization-trace cancellation argument. That argument was not only load-bearing for its own paper. Two other manuscripts, on Kuga-Satake correspondences and on the rational Hodge conjecture for products of K3 surfaces, used the construction it produced. When the first paper fell, both of the ones standing on it fell with it. Fourteen more manuscripts were revised with proof repairs and corrected dependencies, and thirteen others needed reference fixes.
The headline most people took from this is about trust in AI mathematics, and that is a real question. The one we kept returning to is narrower and closer to our own work: the error was cheap, but the blast radius was not, because the broken result was holding up others that had already been published on top of it.
The cost of a wrong result is everything downstream of it
We produce interdependent artifacts for a living. An agent writes a helper, another writes three call sites that assume the helper’s contract. One agent derives a fact about a data source, and a second builds a transformation on that fact without re-deriving it. A finding becomes a premise, the premise becomes a plan, the plan becomes code. The dependency graph is real whether or not anyone draws it, and most of it is implicit.
The eightfolds incident is what that graph looks like when one node is wrong and the wrongness is not caught before the dependents are built. The retraction count was not one. It was one plus everything that trusted it. The two dependent papers were not themselves sloppy; as far as anyone has said, their own reasoning was fine. They failed because the thing they imported was not checked before they imported it, and a correct argument on top of a broken lemma is still broken.
What makes this the right lesson for us rather than a math-world curiosity is the release policy around it. About 300 of the 719 top-line results, roughly 42 percent, had machine-checked Lean proofs as of the withdrawal. The rest, close to half, were released unconfirmed. OpenAI’s advisory group had recommended publishing without waiting for full formalization, and the eightfolds paper was in the unconfirmed set. So this was not a case of a verified result turning out wrong despite the check. It was a case of shipping ahead of the check, at volume, and letting other work accumulate on nodes whose status was “not yet verified.”
A fleet of agents hits this exact shape constantly. Generation is fast and cheap now, and the batches are large. If verification runs behind generation, and dependents get built against results that have not cleared it yet, then the first confirmed error does not cost you one artifact. It costs you the subtree. The number of things you have to walk back is a function of how much you built on unchecked work, not of how bad the original mistake was.
Verify in dependency order, not in submission order
We wrote earlier that once generation got cheap, verification became the job. The eightfolds cascade adds a second clause: not just that you verify, but when, relative to what depends on what. A result that nothing else rests on can wait for its check. A result that other results will be built on cannot, because every hour it sits unverified is an hour during which dependents accrue against it.
Practically, for our own pipelines, that means three habits.
First, the load-bearing nodes get checked before anything consumes them. If an agent’s output is going to be a premise for other agents, it clears verification before it is published as available, not after the batch is done. The order of checking follows the dependency graph, not the order things were produced.
Second, verification status travels with the artifact. A result is not “done” or “not done.” It is confirmed, or confirmed-by-a-second-party, or unconfirmed, and a consumer is entitled to know which before deciding to build on it. The failure in the math release was partly that the repository mixed formalized and unformalized results under one banner of progress, so a reader could not tell from the top line whether a given claim was standing on a kernel-checked proof or on a plausible manuscript. Cornell’s Alex Townsend made exactly this point: the Lean-verified results should have been announced first, and separately. In our systems the equivalent is a status field that is honest and visible, so an agent reaching for a peer’s result knows whether it is standing on a check or on a guess.
Third, we treat “cannot be reproduced” as “not verified.” The model that produced these results is not released, the prompts were not published, and only average compute figures were given. MIT’s Andrew Sutherland put the consequence plainly: treat any claim about one-shotting these problems with a single agent as unverified until the model is available. An output you cannot regenerate from a recorded input is not a result a second party can confirm. It is an anecdote with a number attached. For us the recorded input is the whole point of an audit trail: the prompt, the inputs, the versions, enough that the same artifact can be produced again and checked by something other than the thing that made it.
The opposite of the proof nobody read
A month ago we wrote about a fleet of agents proving Fermat’s Last Theorem in Lean, thirteen million lines no human will ever read. The trust there came from a total check the team waited for: every proof step accepted by the kernel, the final statement matched against a known one, the coordination itself happening at checked theorem statements. No agent built on a peer’s result until the kernel had accepted it, so the dependency graph was verified in place as it grew.
This release is the same machinery run with the checking turned down. Same domain, same formal target, similar scale of output. The difference is entirely in the discipline around publishing: one waited for the check and composed only at checked nodes, the other shipped half-confirmed and let dependents form on nodes that had not cleared. The second produced a cascade the first was structurally immune to. That contrast is the whole lesson, and it has nothing to do with how good the model is. A better generator makes the batches bigger, which makes the ungated dependency graph more dangerous, not less.
Acting quickly on the error, as OpenAI did, is the right reflex and worth crediting. But the cheaper move is upstream of the retraction: do not let anything be built on a result until the result has been checked, and make the unchecked ones impossible to mistake for the checked ones. The sign error was going to happen. Whether it took two other papers with it was a choice about ordering.