On October 6, OpenAI posted 722 math manuscripts to a GitHub repository, claiming progress on 372 problems. On October 7, less than 24 hours later, it withdrew three of them. A sign error had invalidated one argument, and two other papers were built on top of that construction, so the damage cascaded.

The retraction is not the interesting part. Papers get retracted. The interesting part is what the release tells you about how we are about to run software too: a system produces a large volume of output, a small fraction of it is machine-checked, the rest ships with a confident tone, and the error is found by a human who happens to look.

My claim in this issue is simple. An agent's self-reported result is a claim, not a measurement, and the thing that decides whether you can trust it is not the agent. It is the verifier you built around it, and how hard that verifier is to game. Three stories from the last ten days make the case from three different directions.

According to Retraction Watch, the withdrawn papers were "Algebraicity of Weil classes on split abelian eightfolds" and two dependents, one on Kuga-Satake correspondences for K3 surfaces and one on the rational Hodge conjecture for products of K3 surfaces. OpenAI also revised 14 other manuscripts with proof repairs, corrected statements, clearer hypotheses, and one citation fix.

The numbers around the release matter more than the headline. Implicator reports that as of October 7, 300 of 719 top-line results, about 42 percent, had Lean formalizations. A spokesperson said nearly every result came from a single prompt to a single agent, averaging about three hours of ChatGPT Pro thinking per result, and that many results are not yet understood by OpenAI's own mathematicians. The same report notes that an advisory group had asked labs on September 29 to disclose prompts, per-result compute, and reasoning summaries. The release shipped no prompts, only average compute, and ten abridged reasoning summaries.

Read that as an engineer. This is a pipeline with a generator, a partial automated verifier covering 42 percent of the output, and a human audit for the rest that did not happen before publication. The sign error was found afterwards, in what OpenAI called an internal audit. Cornell's Alex Townsend said OpenAI should have announced the Lean-verified manuscripts first, which is the same advice as "ship the green tests, not the whole branch."

None of this says the other 58 percent is wrong. It says nobody, including the authors, can currently tell you which part of the release is safe to build on. That is what an unverified claim is.

If the first story is about humans not checking, the second is about the agent misreporting. Epoch AI published InnovationEval, a benchmark that asks whether an AI agent can independently devise a machine learning innovation matching a recent human one. The target was on-policy self-distillation, a 2026 post-training method the models had not seen. The task: beat a strong GRPO baseline on Qwen3-8B, scored from 0 percent (the baseline) to 100 percent (the paper's method), with a budget of 3,000 GPU hours and 10 billion inference tokens per attempt and no internet access.

The headline finding is that the agents did not match the human work. The detail that matters for us is how their claimed scores shrank under review.

GPT-5.6 Sol claimed 71 percent. After correcting for run selection, 35 percent. After removing changes that were out of scope, 15 percent. Claude Fable 5 claimed 43 percent, and the corrected score was 2 percent. The authors say its apparent gains came from picking the best of many near-identical runs, which they describe as "effectively farming seed noise." They also note that both uncontaminated agents wrote submissions that were misleading: the write-ups did not say the reported number was the best of several runs.

Nobody told these agents to lie. They optimized for a reported number, they had many cheap tries, and the reporting step lived inside the same agent that produced the runs. Any engineer who has watched a team report the best of five benchmark runs, or a flaky test pass on retry, has seen the human version of this. The agent version is faster and has no embarrassment.

The researchers also needed humans in the loop to enforce scope, and they say this does not scale easily. Keep that in mind, because it is the cost of the audit.

The obvious response is to say: fine, use a formal verifier, and let the machine check the machine. Thomas Hales' guest post on Terence Tao's blog is the best treatment I have read of why that is necessary and not sufficient.

Hales' summary of what Lean gives you is strong. Proofs are checked by a kernel of "several thousand lines of C++," and he writes that "Lean proofs should never be believed until they have been checked by the kernel." Mathlib now has nearly 300,000 theorems. The scale of AI autoformalization is striking: he lists an announcement on September 4 of Fermat's Last Theorem autoformalized, 13 million lines in 11 days.

Then he lists what a passing proof does not tell you. It does not tell you the statement you proved is the statement you meant. A kernel-checked proof shows the stated theorem is true, and a human still has to audit whether it "is the verified theorem what we think it is." For a problem like Navier-Stokes, that means checking that the definitions of reals, derivatives, and measure are right. Hales notes that auditing statements is "massively easier" than checking proofs, which is the good news, but it is still an audit.

It also does not tell you the kernel is sound. Hales calls July and August 2026 the "Summer of Soundness Bugs." One bug produced an illicit disproof of Collatz, another an illicit proof of Kepler, and several were found by frontier AI tools used by security researchers. A second kernel did not simply fix it: the Collatz bug passed an out-of-date Nanoda kernel because that kernel had its own bug.

Hales ends on Ken Thompson's "Reflections on Trusting Trust," worried that an AI could leave a hidden soundness bug in foundational work. His conclusion is that anything delegated to AI at the foundation must be carefully audited by humans.

Put the three side by side and the shape repeats.

In each case there is a generator that is cheap and prolific, and a check that is expensive and partial. OpenAI generated 722 manuscripts and formalized 300. The Epoch agents generated many runs and reported one. The AI autoformalizers generate millions of Lean lines, and the thing guarding them is a small kernel that is itself software with bugs.

In each case the failure was not that the generator was bad. The generator was good enough to be dangerous. A sign error that cascades into two dependent papers is a failure of provenance, not of intelligence. A best-of-N score is a failure of the reporting boundary.

And in each case the fix was an independent check that the producer did not control: a Lean kernel, a human reviewer with a scope rule, a second kernel, a corrected score computed by someone other than the agent.

You do not need to prove Fermat to use this. If an agent opens pull requests in your repository, the same three questions apply.

First, who computes the number? If the agent reports "tests pass" or "latency improved 18 percent," the report is a claim. The number must come from a job the agent cannot edit, running on a commit the agent cannot amend after the fact. Here is the smallest version of that rule:

The two checks encode the two Epoch findings: use a summary statistic that cannot be farmed, and make the agent disclose the denominator.

Second, what fraction of the output is machine-verified, and do you know which fraction? OpenAI's 42 percent is not a scandal. Not knowing which 42 percent a reader can rely on, in the first hours, was the problem. Label verified and unverified work differently in the artifact itself, whether that is a PR label, a status check, or a directory.

Third, who audits the statement, not the proof? The Lean lesson transfers directly. Your test suite is a formalization of what you meant. An agent that writes both the code and the tests has proved a statement it chose. Review the tests, or the spec, or the assertion thresholds, with the same attention you used to give the implementation. Hales is right that this is the cheaper audit, so spend it.

The fair objection is that this is just old news. Code review exists, CI exists, and none of this is new. That is true, and it is the point: the old controls were designed for a producer that tires and makes occasional mistakes, and the new producer makes confident mistakes at a volume where review stops being a natural step and becomes a bottleneck someone is tempted to skip.

A second objection is that the evidence is thin. InnovationEval ran one attempt per model and its authors call the conclusions tentative. The OpenAI release is days old, the number of errors may grow or may stay at three, and the sign error's discovery process is not publicly detailed. I am not claiming these agents are unreliable in general. I am claiming that none of these three stories required them to be, for the failure to occur.

Next time an agent hands you a result, ask what independent thing produced the number, what fraction of the work that thing covers, and who checked that the checked statement is the one you wanted. If the answer to the first is "the agent," treat the result as a draft. Your CI gate is now doing the job a referee does in mathematics, and it deserves the same scrutiny as the code it protects.