The Verification Bottleneck

So OpenAI dropped a big pile of math proofs on Oct 6 2026, and this has caused a huge response in the math community. Some of the hotly debated topics are:

1. The work has been done without enough details released. OpenAI released neither the model nor the prompts, so others can’t reproduce the results, and the papers OpenAI released may contain errors. In fact, OpenAI withdrew three papers less than 24 hours after the release due to errors.
2. OpenAI seems to shift the burden of verifying the work onto the community of mathematicians. Only about 42% of the main results have been verified by the theorem prover Lean. It’ll take a long time for the mathematicians to review the AI’s output, and there are not enough resources devoted to that.

In this post, let’s focus on the second topic: the heavy burden of reviewing the deluge of AI’s outputs. This is actually not unique to math. The same has been happening in other fields. In software development, vibe coding is fast and easy, but reviewing the flood of pull requests (PRs) is very taxing. For popular open source projects that can get PRs from anybody in the world, GenAI has increased the number of PRs submitted for reviewing. The gatekeepers of these projects have to deal with the flood of PRs to ensure they work as expected, not going to damage other parts of the code or contain security bugs.

In academic publishing, the same problem occurs as AI is more involved in conducting research than ever. There are so many papers being submitted, and there are not enough reviewers. ICLR received more than 40,000 submissions for 2027, it was just under 20,000 in 2026, and only about 500 in 2016. To overcome the large number of submissions, ICLR 2027 will cap every author at 20 submissions, and researchers without a prior paper at a major conference are limited to a single submission unless a co-author qualifies as a reciprocal reviewer.

At this rate, there will not be enough eyeballs to review the AI’s outputs, and that’s a key issue in the age of GenAI. There are a few ways to deal with this problem based on the nature of the field.

Math is the cleanest case, because a Lean proof certifies correctness with no human reviewer needed. Code is in the middle: tests catch some regressions but not bad design or subtle security flaws. Peer review is at the far end, with almost no mechanical check for whether a paper is novel or meaningful.

Because of these differences, there are different solutions. Where verification can be automated, the fix is to make it the price of admission: require Lean proofs for math results, or passing tests for PRs. That shifts the verification cost back onto whoever is generating the output. Even then, a machine check isn’t the whole story. Lean confirms that the formal statement was proved, but a human still has to confirm that the statement says what the paper claims, and judge whether the result matters.

Where verification can’t be automated, institutions fall back on rationing. ICLR’s 20-paper cap is the blunt version. Its reciprocal-reviewer rule is subtler, because it’s also a price of admission, paid in reviewing labor instead of proofs: if you want reviewers’ time, you have to give some of yours.

I expect AI output to earn trust first in fields where verification is cheap. As generating answers becomes nearly free, the scarce skill will be certifying them.