News

AI Was Supposed to Make Scientists Faster. Now It May Be Making Discoveries.

• By John K. Waters
• 09/09/2026

For most of the generative AI boom, the case for putting artificial intelligence into science has sounded a lot like the case for putting it everywhere else: AI could make researchers faster.

It could search the literature, write code, analyze data, and automate tedious work. The scientist would still do the science; the machine would help clear the desk.

That distinction is beginning to look less secure.

On Tuesday, OpenAI published what it says is an AI-generated solution to the Navier-Stokes existence and smoothness problem, one of mathematics' seven Millennium Prize Problems.

This problem concerns equations that describe fluid motion and has resisted resolution for roughly 90 years. OpenAI's proposed proof argues that an initially smooth fluid can develop a singularity, essentially a mathematical breakdown in which velocity grows without bound in finite time. The company released both the proof and a computer-checkable formalization written in the Lean proof assistant.

(Lean is a software tool that translates mathematical reasoning into formal logic and checks, step by step, whether a proof actually holds.)

That is an extraordinary claim, and it should be treated as one.

A proof of a Millennium Prize Problem does not become established mathematics because an AI company publishes it. It has to survive scrutiny by mathematicians with expertise in the field. OpenAI itself says it does not intend to claim the associated Millennium Prize.

Controversy also surrounds the circumstances of the discovery. WIRED reported that mathematician Tristan Buckmaster has challenged OpenAI's account of how the work developed and raised questions about credit after OpenAI learned that he and Anthropic researcher Levent Alpöge had made progress on a related problem. OpenAI says its researchers and agents did not see their work before completing its own proof.

But even with those qualifications, something interesting is happening.

The important part may not be whether this particular proof ultimately enters the mathematical canon. It is that several frontier AI systems are beginning to behave less like unusually capable research assistants and more like participants in research itself.

Ten Thousand AI Agents Go After a Math Problem
The system that produced OpenAI's Navier-Stokes result was not simply GPT-6 Astra, the frontier model OpenAI released last week.

OpenAI says it used an internal model still in training that is “significantly more capable” than Astra. The company organized agents powered by that model into groups that could communicate, use code, and consult a cached version of the internet. The group that ultimately produced the Navier-Stokes result involved about 10,000 concurrent agents.

This was computation on a very different scale.

OpenAI says the agents working across the attempted problems exchanged 4.9 million messages and generated about 300 billion output tokens. The Navier-Stokes effort alone accounted for roughly 130 billion output tokens and 2.7 million messages. The agents arrived at the proposed solution after about 88 hours, followed by another 17 hours of formalization and verification using Astra.

In other words, this wasn't one chatbot sitting down and having a Newton-under-the-apple-tree moment. It looked more like a computational research organization.

Different groups explored different versions of the problem. Agents pursued competing approaches. Results were shared between groups. OpenAI says it used Codex to consolidate promising ideas so other agents could build on them.

That may be as consequential as the proof itself.

The emerging unit of AI-assisted research may not be one scientist talking to one extraordinarily intelligent model. It may be a human directing thousands of artificial researchers that can explore hypotheses in parallel, criticize one another's work, discard failed approaches, and keep going.

Claude Has Been Doing Some Math, Too
OpenAI isn't alone.

Last month, Anthropic reported that an unreleased version of Claude had been asked to take a serious run at the Riemann hypothesis, another Millennium Prize Problem and one of mathematics' most famous unsolved questions. (The Riemann hypothesis proposes a specific pattern in the distribution of prime numbers, the numbers divisible only by themselves and one.)

Claude didn't solve it.

Instead, according to Anthropic, the model unexpectedly improved a longstanding lower bound related to the zeros of the Riemann zeta function from 41.6 percent to 67.2 percent. Two Anthropic mathematicians examined the work, outside experts reviewed the paper on short notice, and Claude also produced a formally verifiable version of the result.

The path it took sounds remarkably similar to OpenAI's approach.

Anthropic says Claude initially generated 650 ideas that went nowhere. It then coordinated roughly 60 subagents, which ran thousands of numerical checks, wrote hundreds of Python scripts, reviewed one another's work, searched for counterexamples, and eventually produced the new result.

Then, last week, Anthropic announced another milestone: Claude had produced what the company describes as the first complete computer-checked formalization of Fermat's Last Theorem. Unlike the Riemann-related work, this was not new mathematics. Andrew Wiles proved the theorem in the 1990s. The achievement was converting the enormous body of reasoning behind that proof into a form that the Lean proof assistant could check from end to end.

Anthropic says a multi-agent system completed the work in less than two weeks, generating 13 million lines of Lean and proving 29,500 intermediate theorems. Mathematician Kevin Buzzard, who has led a community effort to formalize Fermat's Last Theorem, called the result an “extraordinary autoformalization achievement.”

These are different accomplishments. Formalizing an existing proof is not the same as discovering a new one. Taken together, however, they point in the same direction.

The Verification Problem
Machines that can generate mathematics at enormous scale face an obvious problem. Somebody has to determine whether the mathematics is right. This is where formal verification becomes unusually important.

A conventional mathematical proof is written for other mathematicians. They read it, challenge its assumptions, examine the steps, and eventually decide whether the result holds.

A formal proof translates that reasoning into a language that a proof assistant such as Lean can mechanically check against a set of mathematical axioms and previously established results.

That doesn't make every scientific claim automatically trustworthy. It does, however, provide something generative AI desperately needs: a domain in which at least part of its output can be subjected to rigorous machine verification.

This creates a fascinating feedback loop. AI systems can generate enormous quantities of candidate mathematical reasoning. Other AI systems can attempt to criticize or formalize it. A proof assistant can then mechanically reject steps that don't follow.

Anthropic explicitly argues that automated formalization could become increasingly important as AI produces more mathematical work because human verification can take months or years. If AI dramatically increases the supply of proofs, verification may become the scarce resource.

From Productivity to Discovery
Mathematician Terence Tao has been thinking about what mathematics might look like if research-level AI becomes commonplace. In an essay based on his 2026 International Congress of Mathematicians lecture ("Mathematics in the Age of AI"), Tao largely sets aside the argument over whether AI will eventually acquire such capabilities and asks what happens to mathematics if it does.

That's increasingly the useful question. For years, the economic argument around generative AI has revolved around productivity: How much faster can a programmer write software? How many documents can an employee produce? How much customer service can a company automate?

Scientific research presents a different test. If an AI system reorganizes a literature review in seconds, that's productivity. If it writes the Python scripts a scientist would otherwise have written, that's productivity.

But if a system explores thousands of possible approaches to an unresolved mathematical problem, identifies one that works, and produces a result humans didn't previously know, something different has happened. The machine has contributed to the creation of knowledge.

That doesn't mean scientists disappear, of course. The OpenAI and Anthropic examples actually suggest something considerably messier. Humans chose the problems. Humans built the systems. Human researchers examined the results. Existing mathematical literature supplied much of the intellectual foundation, and formal tools helped establish whether particular chains of reasoning held together. OpenAI's Navier-Stokes result still faces the most important test of all: scrutiny from the mathematical community.

But the AI system's role is getting harder to describe as mere assistance. And OpenAI is already signaling that what comes next may move faster. The company says the internal model behind the Navier-Stokes work is still being trained and is substantially more capable than Astra.

That may ultimately be the bigger news than whether one famous equation has finally been cracked. For the first few years of generative AI, we asked whether machines could reproduce things humans already knew how to create.

Now researchers are beginning to confront a more consequential question.

What happens when they start finding things we didn't know?