AI Output Verification at Scale Needs a Record of What Was Checked

On October 6, OpenAI put 722 mathematics manuscripts on GitHub, written by an internal model it has not released.^[1] The model was pointed at about 4,000 problems, and each result took about three hours of ChatGPT Pro thinking compute.

On October 7, OpenAI withdrew three of the papers for a sign error, repaired 14 more, and logged every change in a public history file.^[2]

The coverage has treated this as a mathematics story. We read it as the first public, full-size example of a situation every team running agents is building toward: more output than anyone can check, a mix of checked and unchecked inside it, and a recipient who inherits the difference.

What did OpenAI release, and how much of it was checked?

OpenAI released 722 manuscripts in 372 families of results, from an unreleased model pointed at about 4,000 problems. By OpenAI's own count, about 42 percent of the top-line results are formalized in Lean, a proof assistant that machine-checks a proof. An OpenAI spokesperson told Retraction Watch that roughly half the results went out unconfirmed.^[3]

The prevailing read is that this was a dump:

• New Scientist's headline says OpenAI "must clean up the mess."^[4]
• The Atlantic's says OpenAI "carpet-bombed mathematics."^[5]
• A statement from the Association for Human Mathematics calls releasing over 700 files at once "not a demonstration of scholarship."^[6]
• The advisory group of mathematicians OpenAI consulted said its role "should not be interpreted as" an endorsement of the process.^[7]

Cornell's Alex Townsend put the practical objection to Retraction Watch: OpenAI "should have announced the manuscripts that were lean verified first," and asked for help with the rest separately.^[3]

All of that is fair. The checking burden is real, the prompts were withheld, and the model is unreleased. Our disagreement is with the diagnosis: the failure sits at the gate, not in the volume.

Why is this a builder's problem?

A model that produces 722 results in a few weeks outruns any reviewing community, paid or volunteer. The only thing that scales with the output is the record: per item, what was checked, by what, and what was not. Every team running agents is building the same situation at a smaller scale.

Think about what an agent pipeline hands to the next person. A batch of pull requests. A folder of generated reports. A queue of candidate findings. Some were tested, some were looked at, and some were neither, and the recipient usually cannot tell which is which.

We have written before that AI output quality depends on who is checking. This release is that problem with a community of experts as the recipient and a public argument about who should have done the checking.

What did OpenAI's record get right?

The release carries a per-result formalization catalogue, versioned corrections with earlier editions preserved, a public history file, and a withdrawal inside 24 hours. That is a three-valued record: formally checked, released unformalized, withdrawn. It is more than most agent pipelines write down.

The withdrawal was fast because the record made the error findable. A sign error in one manuscript invalidated an argument that two dependent papers relied on, the dependency was on file, and all three came down together. Fourteen other manuscripts were repaired, and 13 more had their citations updated to point at the revised editions.^[2]

The record is better than most. It is not complete. The README's warning that "some of the unformalized results could have issues" is one line at the top of the repository, not a label a reader sees on each manuscript.^[1]

Where did the release fail?

At the gate. Roughly half the results went out unconfirmed, by OpenAI's own estimate. The model is unreleased, and the prompts the advisory group asked for were not disclosed, so nobody outside can replicate the work. The checking cost moved downstream to unpaid reviewers, and the anger in the coverage is the price of that placement.

MIT's Andrew Sutherland told Scientific American that "we should expect some of the proofs to contain mistakes, possibly serious ones," and that open science means reporting negative results alongside positive ones.^[6] The README says the model was posed about 4,000 problems. The ones it did not solve are not in the repository.

Does a Lean proof mean the result is correct?

It means the proof follows from the statement as written in Lean. It does not show that the Lean statement matches the original problem, or that the result is new.^[8] A verified proof of the wrong statement passes. So even the checked column needs a second label: checked against what.

The counts show the same thing. OpenAI reports about 42 percent of top-line results formalized. Decrypt counted the repository's formalization catalogue and found 162 of 722 papers with a formalized main result.^[8] Both are correct, and they measure different things. A reader of any verification record has to know what each column counts.

What did Anthropic ship two days later?

The same shape, in software. On October 8, Anthropic launched OSS Scanner, which sends vulnerability reports to open-source maintainers that are, in Anthropic's words, "fully model-generated, without human review or triage."^[9] The program is opt-in and free, it is modeled on Google's OSS-Fuzz, and some maintainers asked to receive the unvalidated findings.

Anthropic's own validation is careful. Over six months its models found more than 29,000 candidate vulnerabilities, and its people reviewed about 6,000 of them. Expert testers checked 97 critical and high findings across 48 projects, and 85 met the disclosure bar. wolfSSL reports that 72 of 74 reports were valid and five became CVEs.

The structure is still the one in the mathematics release. A vendor-measured sample validates the pipeline, and the recipient absorbs whatever the sample did not cover, one report at a time.

Can AI checks replace a person reviewing the output?

They can produce a verdict. Whether the verdict separates good output from bad is a measurement, not an assumption. A Carnegie Mellon screen of 13 automated validators on a deployed generative agent found that nine of them could not be told apart from zero.^[10] One deployment, one author, and still the best numbers we have.

Xin Xu screened each validator against what happened downstream: 550 runtime builds labelled broken or acceptable, plus 350 static ones. Two checks separated the classes after correction for multiple comparisons.

Three fired on 96 to 100 percent of everything, so they carried no information. Three never fired on any sampled build. A detector built to catch blank output caught 0 of 90 human-labelled blank builds.

The finding no benchmark would show is in the execution log. Runtime probes were skipped on about one broken build in six and on almost no acceptable build, 144 of 895 broken against 1 of 972 acceptable across four runs, and each skip was recorded as a pass.

"Ran and passed" and "did not run" were the same symbol in the log. That caps what any live check in the pipeline can catch at about 84 percent, however good the check.

One layer up, 32.5 percent of the judge's rejections carried no recorded issue. A third of the "no" verdicts had no reason on file.

That is the measured case for the three-valued record. OpenAI's catalogue, with its checked, not checked and withdrawn entries, is the right shape even where its gate was wrong, because it keeps the third value visible.

How should a team record verification for AI-generated output?

Per item, in three states: checked and passed, checked and failed, not checked. The deliverable is the artifact plus its verification state. The gate is the decision about who pays for the third column: you, a reviewer you staff, or the recipient. Most agent pipelines choose the recipient and never say so.

OpenAI chose the recipient and said so, once, in the README. The agent pipelines we see tend to run the other way: guardrails that check the action but not the premise, approvals that record an absence rather than a review, and a human in the loop who is expected to supply attention the system never asked for.

We have argued that human-in-the-loop is architecture, not vigilance. The record is what that architecture looks like on disk.

Four practices follow, and none needs a new tool:

1. Label every output with its check state, and carry the label to whoever receives it.
2. Keep the errata log where the consumer can see it, with earlier versions preserved.
3. Measure whether your checks separate good from bad. A periodic screen against outcomes, not an inventory of checks that ran.
4. Budget the unchecked share as work still owed, not as done.

The first practice is where the definition of done lives. Writing it down per item is what makes the third practice possible at all.

The 24-hour withdrawal is the system working, and it worked because the record existed. "Actually done" now has a measured counterpart: in one real pipeline, most of the checks could not tell the difference, and nobody could see that from the log. The question for any team shipping agent output is whether anyone downstream can tell what was checked.