OpenAI’s math agents have a proof to answer for

OpenAI has released an analytical proof and Lean formalization for the Navier–Stokes Millennium Prize Problem, saying an internal system of coordinating agents produced the result. The release puts a frontier-model claim into a form mathematicians can inspect; it does not settle the question of formal recognition.

OpenAI says the system used roughly 10,000 concurrent agents, with access to code execution and a cached internet. It says those agents reached a result after about 88 hours, and that GPT-6 Astra then spent another 17 hours on the Lean formalization. The company also released the paper and a public Lean repository.

What OpenAI says it found

The Clay Mathematics Institute’s formulation asks whether smooth, three-dimensional incompressible fluid flow must stay smooth, or whether it can develop a finite-time singularity. OpenAI’s paper argues for the latter: a smooth force can drive a flow from rest toward unbounded velocity while its kinetic energy stays bounded.

That distinction matters. A successful proof would identify a limit in the mathematical model used to describe fluid motion. It would not mean water or air literally reaches infinite speed. OpenAI frames the finding as a solution to alternatives C and D in Clay’s published problem statement.

Lean is evidence, not the final referee

Lean can mechanically check whether a formal proof follows its rules. It cannot by itself resolve every question mathematicians ask about how a long argument was translated, structured, or connected to the original problem. OpenAI’s release is unusually useful for review because it includes both the prose paper and the formalization.

There is early external support for the core mathematical fit. EL PAÍS reported that Charles Fefferman, who wrote Clay’s 2000 formulation, said the result solves the problem as he stated it. The same report said he would need a conventional mathematical rewrite and careful reading by several experts before he was fully convinced.

Credit is part of the story

The public release has also prompted a dispute over prior work. OpenAI says its project began after hearing rumours of progress by Tristan Buckmaster and Levent Alpöge, and says its researchers and agents did not see their unpublished work. It also says it cannot rule out a contribution from de-identified product-usage data to model improvement.

EL PAÍS reported that OpenAI later revised its paper to add citations to work by Diego Córdoba and Luis Martínez-Zoroa. Those attribution questions are separate from whether the proof survives review, but they affect how the result will be received. The next evidence will come from public mathematical scrutiny of the released paper and formalization.