What happens when AI can produce research faster than humans can check whether it’s correct?

That question became a lot more interesting this week.

On October 6, OpenAI published a collection of mathematical results generated by an internal frontier model. The release contains 719 manuscripts organized into 372 families of results, spanning areas including number theory, geometry, topology, probability, and theoretical computer science. GitHub →

These aren’t 372 independently confirmed breakthroughs. They’re a collection of AI-generated research results at different stages of verification.

And that distinction matters.

According to OpenAI, the model was given approximately 4,000 mathematical problems. Each result used, on average, compute equivalent to roughly three hours of ChatGPT Pro thinking. The company also released selected reasoning summaries and formalizations of many proofs using Lean, a language and proof assistant that allows mathematical arguments to be checked by a computer. OpenAI →

The Interesting Part Isn’t Just the Volume

It’s the possibility that AI systems are becoming capable of exploring mathematical problems at a scale that would be difficult for individual researchers to match.

But there’s a catch.

“Generating a proof and verifying a proof are two different problems.”

Lean: Automated Testing for Mathematics

Lean is particularly interesting here.

Think of it as a programming language for mathematical proofs. Instead of asking someone to read an argument and decide whether it makes sense, you express the relevant definitions, statements, and reasoning in a formal system that can check whether the proof follows from its assumptions.

It’s one of the closest things mathematics has to automated testing.

But even that has limits.

A proof assistant can verify the formal statement it receives. That doesn’t automatically establish that the statement faithfully represents what a researcher intended to prove.

And it doesn’t establish that the result is novel, important, or explained well enough for other researchers to understand.

Verification at Different Stages

OpenAI’s own repository acknowledges that its results are at different stages of verification. Approximately 42% of the top-line results had been formalized in Lean at the time of the release. GitHub →

The subsequent review has also exposed problems. In its October 9 report, The Verge described researchers struggling to evaluate the enormous collection. By October 8, OpenAI had revised more than a dozen manuscripts and removed three papers after identifying a sign error that invalidated an argument. Some researchers also raised concerns about whether the formalized statements consistently matched the claims made in the accompanying papers. The Verge →

This doesn’t mean the entire collection is unreliable.

Several mathematicians interviewed by The Verge considered parts of the work genuinely impressive. The problem is that the collection contains results with different levels of quality and verification, and evaluating them takes time. The Verge →

When Formal Proofs Don’t Match Natural Language

There’s also a technical issue worth understanding.

A separate preprint published on October 6 examined the formalization of OpenAI’s earlier Navier–Stokes result. Its authors argue that a Lean proof can be valid while failing to faithfully represent the natural-language argument it is supposed to verify. This is a specific critique of that earlier result, not a verdict on the entire new collection, but it highlights a broader challenge for AI-generated mathematics. arXiv →

The Connection to Software Development

For me, this connects to something much closer to everyday software development.

We already know that AI can generate code faster than we can comfortably review it. A model can produce hundreds of lines of code, write tests, and even suggest fixes for its own mistakes.

But passing tests doesn’t necessarily mean the software does what the user actually needs.

The tests might be incomplete. The requirements might be wrong. The implementation might satisfy the specification while violating an assumption nobody thought to check.

Mathematical formalization has a similar problem: the verification system is only useful if the thing being verified accurately represents the intended claim.

“Passing tests doesn’t necessarily mean the software does what the user actually needs.”

The Next Layer of AI Development

This is why I think the next important layer of AI development isn’t just making models better at producing answers.

It’s building systems that help us check, reproduce, understand, and trust those answers.

For coding agents, that means better testing, stronger specifications, reproducible environments, and meaningful human review.

For mathematical research, it means formal proofs, transparent methods, proper attribution, and enough context for independent researchers to evaluate the results.

Scale as a Challenge

The scale of AI-generated work is becoming a challenge in its own right.

OpenAI can generate hundreds of mathematical research manuscripts, but the research community still needs to understand what they establish, which ideas are genuinely new, and how the results connect to existing knowledge.

And that raises a question I keep coming back to:

“If AI can generate knowledge faster than we can verify it, does verification become the real bottleneck?”

Sources & References