AI agents claim Navier-Stokes as mathematicians push back

OpenAI says 10,000 of its AI agents solved a problem mathematicians have worked on for a century. Three days later, 25 winners of mathematics' highest honor signed a declaration warning about exactly this kind of announcement. Both things happened in the same week, and the gap between them is the story.

Navier-Stokes is a set of equations describing how fluids move. The open question, worth a million dollars, was whether solutions in three dimensions always stay smooth or can blow up. Quanta Magazine reported on September 8 that OpenAI's agents found the blow-up, called a singularity.

What the agents produced

Quanta gives numbers that say as much about the method as the result.

Measure	Figure
Agents running	10,000, autonomous
Time to the proof	88 hours
Time to formalize it	17 more hours
Messages exchanged between agents	Nearly 5 million
Estimated compute cost	Several million dollars

Formalizing a proof means rewriting it so a computer can check every step mechanically. It is the part that lets outsiders trust a result without following the argument themselves. Our earlier report on Anthropic's AI formalizing Fermat's Last Theorem covered the same technique applied to a much older result.

The credit is not clean, and Quanta says so. Tristan Buckmaster and Levent Alpöge announced a related result on the Euler equations twelve hours earlier, also with AI help. Quanta reports a dispute over the timeline and over access to work that came before the announcements. It also credits analytical techniques from Diego Córdoba and Luis Martínez-Zoroa as essential to both efforts.

What the Clay Institute actually said

The Clay Mathematics Institute set the Millennium Prize Problems in 2000, each worth a million dollars. Quanta counts six still open before this claim. It is the body that decides whether one has been solved.

Its statement on September 11 is three careful words long in the part that matters. The problem has "apparently been settled." The institute added that its evaluation follows established rules and is deliberately unhurried.

Nobody has been paid. "Apparently settled" is an acknowledgment that a claim exists and looks serious, not a ruling that it is correct.

Why 25 mathematicians signed a warning

On the same day, Terence Tao published a post about a joint declaration from 25 Fields Medallists. The Fields Medal is mathematics' equivalent of a Nobel Prize.

Their objection is not that the AI results are wrong. It is that AI companies treat mathematical problems as performance benchmarks, and that results arrive announced fast, without proper writeups or citations. That conflicts with how mathematics normally works, where understanding is built through long human exchange.

Tao's framing is the sharpest line in it. He writes that "solving problems is only a tool and proxy for achieving the primary goal of conceptual understanding." The declaration warns that "mass production at faster and faster pace of 'true/false' statements could destroy fertile ground," and that the transmission chain between mathematicians is what is at risk.

What this means for developers

You are the audience for these announcements, so read them the way a reviewer would. Ask three questions of any AI result you see this year. Is there a writeup you could check. Was it formally verified, and against what. Who else was working on it, and were they credited.

Separate verification from understanding, because they are not the same guarantee. A machine-checked proof tells you the steps follow. It tells you nothing about why the result is true or what it generalizes to. If you plug a formally verified AI output into your own work, you have imported a fact you cannot yet explain, and that has a cost when it breaks.

Discount the benchmark framing specifically. The Fields Medallists' complaint is that solved problems are being used as scoreboards, and a scoreboard rewards announcing first. Quanta's account of a twelve-hour gap and a disputed timeline is what that incentive produces. The same pressure sits behind the model benchmark numbers you read when picking an API.

The engineering lesson is the cheapest one to take. Ten thousand agents, five million messages and 88 hours produced something real here, and the artifact that made it checkable was the formalization, not the agents. If you are building multi-agent systems, the transferable part is that the output needs a mechanical check at the end. Without one you have a confident answer and no way to audit it.