AI-generated math proofs: why checking is now the hard part

On October 6, OpenAI published a large set of new mathematical results produced by an internal model it has not released. More than 700 manuscripts went up at once, claiming progress on 372 problems across geometry, algebra, computer science and other fields. The next day, three of them were withdrawn over a sign error. This matters well beyond mathematics. It is one of the clearest public tests yet of what happens when AI produces expert-level work faster than experts can check it.

What was released

OpenAI says the average result used compute equal to about three hours of ChatGPT Pro thinking. Many proofs come with formalizations in Lean, a programming language that lets a computer check a proof step by step. The repository's own notes say about 42 percent of the top-line results are formalized, and that the collection holds results at different stages of verification. An OpenAI spokesperson told Retraction Watch that roughly half of the results were released unconfirmed, after its advisers on mathematics and AI recommended not waiting for full formalization.

On October 7, OpenAI withdrew three manuscripts. A sign error broke the argument in one paper and a construction that two others relied on. It also revised 14 other manuscripts with proof repairs. OpenAI said it found the problems in its own audit and that it welcomes scrutiny from the mathematical community.

How mathematicians responded

Reactions were split. Nature reported that some mathematicians celebrated solutions to long-standing problems, while others complained of being scooped. Ursula Martin of the University of Oxford said the release was "tossing the community a messy first draft and expecting us to clean it up for them." Alex Townsend of Cornell told Retraction Watch that OpenAI "should have announced the manuscripts that were lean verified first." Andrew Sutherland of MIT called the quick withdrawals "the responsible thing to do."

Capability was never the only question

Whatever one thinks of the release, it shows the gap between capability and reliability very clearly. The model can produce work that looks like serious mathematics, at a pace no research group could match. But a result is only useful once someone can trust it. Here, that trust has to be built paper by paper, by people with years of training in each specialty. Producing the work took hours of compute. Checking it will take far longer, and the people able to do it are few.

Machine checking helps, but it does not settle everything. Lean confirms that a proof is valid for the statement as it was written down in Lean. Whether that statement is the problem people actually care about, and whether the result is new, are questions a person in the field still has to answer.

A proof checker can tell you the argument is valid. Only an expert can tell you it answers the right question.

Lessons for anyone checking AI work

The same pattern is spreading far beyond mathematics. Code, legal drafts, research reports and medical summaries can all be produced faster than they can be reviewed. A few habits from this episode carry over:

• Rely first on the work that has been checked, and say plainly which parts have not.
• Use automatic checks where they exist, and be clear about what they cover and what they miss.
• Put reviewers who know the field on the outputs that matter, and measure how often they catch real errors.
• Turn every error found, even a single wrong sign, into a test case for the next run.

The sign error is a useful reminder. One small mistake undid three papers because other work was built on it. In long chains of AI work, an early error travels.

What this means in practice

For teams that build or rely on AI, the bottleneck is moving from producing work to verifying it. Plan for that before the work starts. Decide who will check it, how, and what counts as a pass. Keep a record of what was verified and by whom. At SoReliable, we think expert review belongs inside the system, measured and trained like any other part of it, rather than left as a cleanup job for whoever receives the output.