on navier stokes

On September 8th, 2026, OpenAI casually announced that roughly 10,000 AI agents had resolved the Navier–Stokes Millennium Prize Problem after working for approximately 88 hours and spending a few small loans of a million dollars on compute.¹²

I looked into it more, and the proposed proof does not appear to prove case (A) of the formal problem statement, the strongest version, which asks one to show that a fluid can never break down on its own, without any outside force. Instead, it claims to prove case (C), which lets one design a specific outside force that causes the fluid to break down.

the problem statement

The incompressible Navier–Stokes equations on $\mathbb{R}^3$ are

$$\begin{aligned} \partial_t u + (u \cdot \nabla) u &= -\nabla p + \nu \Delta u + f, \\ \nabla \cdot u &= 0, \\ u(x, 0) &= u_0(x). \end{aligned}$$

Fefferman’s official statement³ defines four ways to win, of which two are of primary importance.

(A) Set $f \equiv 0$. For every smooth, divergence-free, rapidly decaying $u_0$, prove there exist smooth $u, p$ on $\mathbb{R}^3 \times [0, \infty)$ with bounded energy:

$$\int_{\mathbb{R}^3} |u(x,t)|^2 \, dx < C \quad \text{for all } t \geq 0.$$

(C) Show there exist a smooth $u_0$ and a smooth, rapidly decaying force $f$ for which no such solution exists.

Note the quantifiers: (A) is a statement about all initial conditions, with the forcing fixed at zero. The fluid has to behave on its own, forever, no matter how you start it. (C) is a statement about one pair $(u_0, f)$, and $f$ is yours to choose. The force stops being part of the problem and becomes part of the solution. Any error term the construction cannot control, one can try to absorb into $f$, as long as $f$ stays smooth and decays.

It is clear to me why (C) fell first. It’s arguably much more computationally tractable than (A). It’s a search problem: find one construction and check it, and OpenAI’s construction does just that. The force is smooth and compactly supported, the velocity is smooth for $t < 1$ with finite energy, and $|u|$ becomes unbounded as $t \to 1$. It adapts a blowup method Diego Córdoba and Luis Martínez-Zoroa developed in 2023 for related fluid equations.⁴

The version most people mean which concerns the fluid just being left alone is still open.

Now, I don’t want to undersell this result. If this holds up under peer review, it still represents a massive step change in intelligence. I mean seriously, 4 years ago they could barely do a child’s math homework.

suppose one has four pigeons and six holes

Navier–Stokes is the largest entry in a list that has been growing all year:

Result	Date	Kind	What it built on
Cap sets (FunSearch)5	Dec 2023	Construction	Largest improvement in 20 years to the asymptotic lower bound
”10 Erdős problems” (GPT-5)6	Oct 2025	Literature search	Every solution already existed in published papers
Borsuk’s conjecture, $n = 63$7	May 2026	Counterexample	The 2014 Jenrich–Brouwer construction, plus one additional point
Jacobian conjecture, $n = 3$8	Jul 2026	Counterexample	Open since 1939. Explained geometrically by humans days later
Sendov’s conjecture9	Aug 2026	Proof	Elementary methods. Days of human work to make it readable
Navier–Stokes, forced case1	Sep 2026	Construction	Córdoba and Martínez-Zoroa’s 2023 blowup method

The first is how many of these are counterexamples

The second is how often the understanding came afterward, from humans.

The Jacobian counterexample, credited by Alpöge of Anthropic to Claude, arrived as an explicit polynomial map. It was correct and easily verifiable. However, Tao wrote that “the construction … appears like a massive miracle.”¹⁰ It took David Speyer’s geometric explanation, and Tao’s own rewrite, to show why it worked.¹¹

The Sendov proof, generated with GPT-5.6 Pro, was correct. Tao wrote that it had taken him “several days (with heavy AI assistance)” to digest it, “to place the proof in proper context with previous literature and to simplify and streamline the argument to highlight the main ideas.”⁹

The Borsuk counterexample is the clearest case of all. The prior record was a 64-dimensional construction from 2014. The new one takes that same core and adds a single point.¹²⁷

A counterexample is an object. One constructs it, and then checks it.

It appears to be the case that these are the kinds of problems current AI systems are best at. Exhaustively search constructions, combine known techniques, verify, discard what fails, and repeat, ten thousand times in parallel.

Proving that something always holds is quite a different problem. A regularity condition for Navier–Stokes would need an idea for why blowup cannot happen. There is nothing to search for, necessarily; one just has to come up with a new idea after thinking hard enough.

Now, the pattern is not absolute. Sendov’s conjecture is a universal statement, and a machine proved it. But Tao also described that proof as “remarkably elementary.”⁹ It was an argument that seemed to be always within reach, it had just not been assembled yet.

I don’t think it is an accident that the first Millennium Problem to fall to machines fell in the direction of a construction.

When I read about how this was done, it’s difficult for me to believe if the AI system really did anything to understand the fluid.

It is genuinely hard to tell. The output is correct, or at least it passes a proof checker. But the process looks less like insight and more like very fast, very wide recombination. Take an existing result, adapt it, connect it to another, and keep going until the conjecture died.

Additionally, the proof itself is not objectively clear, which does not help given that there are perhaps 10 people in the world with the expertise to verify it.

It seems to be the same pattern again: the machine produces the object, and a human produces the explanation.

I am not certain that will last. But a correct proof is not evidence of understanding, and we should stop treating it as if it were.

why we need to be r i g o r o u s

The natural response for one to come to is to conclude that learning mathematics deeply is less important now, though I think the opposite may be true.

OpenAI’s proof comes with a formalization in Lean.⁴ Lean’s kernel does not accept a proof with a gap, but it does accept a proof of the wrong theorem and a wrong formalization.

Formal verification checks that the proof matches the statement and it says nothing about what you meant. Deciding if the definitions are correct, if the hypotheses are too strong, or if the result even answers the question being asked requires a deep understanding which cannot and should not be delegated to the thing being checked.

If machines are going to produce most proofs, I suppose the human role will shift. Rather than developing new ideas, one would be in charge of verifying them.

sipping lean?

I suspect that within a decade, a mathematician who cannot read and write formal proofs will be in the position of a programmer who cannot code: a really bad one.

Now, I suppose the good part of that is the fact that Lean forces a high level of rigor. One cannot wave their hands at a proof assistant, pray to the lord, and get a proof. Every step must be rigorously defined.

---

Footnotes

1. Quanta Magazine, AI Has Solved One of Math’s $1 Million Millennium Prize Problems  (Sep 8, 2026). ↩ ↩²

2. OpenAI, On the Navier–Stokes Millennium Prize Problem  (Sep 2026). ↩

3. C. Fefferman, Existence and Smoothness of the Navier–Stokes Equation , Clay Mathematics Institute. ↩

4. Wikipedia, Navier–Stokes existence and smoothness . ↩ ↩²

5. B. Romera-Paredes et al., Mathematical discoveries from program search with large language models , Nature 625 (2024). ↩

6. The Decoder, Leading OpenAI researcher announced a GPT-5 math breakthrough that never happened  (Oct 2025). ↩

7. An AI Generated Counterexample to Borsuk Problem in Dimension 63 , arXiv:2608.12561 (2026). ↩ ↩²

8. Counterexamples to the Jacobian conjecture in dimensions greater than two , arXiv:2608.00222 (2026). ↩

9. T. Tao, A digestion of the proof of Sendov’s conjecture  (Aug 2026). ↩ ↩² ↩³

10. T. Tao, A digestion of the Jacobian conjecture counterexample  (Jul 2026). ↩

11. Wikipedia, Jacobian conjecture . ↩

12. T. Jenrich, A. E. Brouwer, A 64-dimensional two-distance counterexample to Borsuk’s conjecture , Electron. J. Combin. 21 (2014). ↩