The Navier-Stokes Situation pt2

12 Sep, 2026

In Part I, I wrote about Navier-Stokes.

The equation is

\frac{\partial 𝐮}{\partial t} + (𝐮 \cdot \nabla) 𝐮 = - \frac{1}{ρ} \nabla p + ν \nabla^{2} 𝐮,

with

\nabla \cdot 𝐮 = 0 .

The question was whether smooth initial data

𝐮 (𝐱, 0) = 𝐮_{0} (𝐱)

can ever evolve into a singularity in finite time.

In slightly less respectable mathematical language:

can water blow up?

I ended with:

We went looking for the equation of water.

We found it.

Now we have to figure out what the equation knows.

This was perhaps poorly timed. Because on September 8, 2026, OpenAI announced that an internal AI system had produced a solution to the Navier-Stokes existence and smoothness problem.

And the answer, apparently, is yes. Water can blow up.

Maybe.

Welcome to Part II.

88 hours

The Navier-Stokes regularity problem has resisted mathematicians for generations.

It is one of the seven Millennium Prize problems. Solve it and the Clay Mathematics Institute has $1 million waiting for you, although inflation has spent the last quarter century making the prize increasingly symbolic.

Only one Millennium problem has been solved so far: the Poincaré conjecture.

Grigori Perelman solved it and then refused the money. Extremely mathematician behavior. Navier-Stokes remained.

Then OpenAI apparently pointed an enormous amount of compute at it. The story begins around September 1.

There were rumors circulating that major progress had been made on two Millennium Prize problems. OpenAI had also apparently observed a jump in the capabilities of an internal mathematical reasoning system.

So they did the obvious thing. They launched thousands of agents against the Millennium Prize problems. This is already a sentence that would have sounded completely ridiculous five years ago.

The agents were also assigned easier mathematical problems. One of them produced a result on a regularity problem for the Euler equations, which are closely related to Navier-Stokes.

That was enough of a signal I guess. Resources were redirected toward Navier-Stokes.

Then:

88 hours

and roughly

3 \times 10^{11}

output tokens later, the system produced a claimed solution.

Three hundred billion tokens. If you take the source's rough conversion, that is around 225 billion words and roughly $22.5 million of compute. The prize is $1 million.

We may have discovered the first mathematical proof with a gross margin of approximately negative 2,150%. I respect this enormously.

What did it supposedly prove?

There is an important distinction here. The popular description of the Navier-Stokes problem is usually something like:

Given smooth initial data, does the solution remain smooth forever?

Symbolically,

𝐮_{0} \in C^{\infty} ⟹ 𝐮 (\cdot, t) \in C^{\infty} \forall t > 0 ?

A counterexample would instead produce some finite time $T$ such that a relevant norm becomes unbounded:

{lim sup}_{t \to T^{-}} ‖ 𝐮 (\cdot, t) ‖_{X} = \infty .

Very loosely:

smooth \to smooth \to smooth \to oh no .

But there is a subtlety. The Clay formulation includes variants involving a smooth external forcing term.

Instead of

\frac{\partial 𝐮}{\partial t} + (𝐮 \cdot \nabla) 𝐮 = - \nabla p + ν \nabla^{2} 𝐮,

consider

\frac{\partial 𝐮}{\partial t} + (𝐮 \cdot \nabla) 𝐮 = - \nabla p + ν \nabla^{2} 𝐮 + 𝐟 .

Here $𝐟 (𝐱, t)$ is a smooth external force.

The question then becomes whether one can construct smooth initial data and smooth forcing such that the resulting solution nevertheless develops a singularity in finite time.

According to the account surrounding the announcement, this forced blowup route is where things became interesting.

And where things became extremely messy.

There were already two mathematicians in the room

Tristan Buckmaster and Laurent Alpe-something had already been working on closely related ideas.

Their work itself followed earlier work by Diego Córdoba and Luis Martínez-Zoroa on using the forcing term as a route into the problem.

This matters because forced blowup was apparently not the fashionable attack on Navier-Stokes. Most people were not working on it. Then OpenAI spends a few days on the problem and arrives in roughly the same strange neighborhood.

Buckmaster called this a bright red flag. Not proof of anything. A red flag. There is an important difference here. Buckmaster was careful about this. His position was essentially:

I have not seen OpenAI's proof.

I don't know what their model did.

I don't know whether our data was used.

I am not accusing anyone of anything.

But the coincidence is sufficiently strange that I would like to know what happened.

This is reasonable, I'd say.

If ten thousand mathematicians are digging in field A and you have privately discovered that the gold is actually underneath one extremely specific tree in field B, and three days later a machine with access to half the world's mathematical literature arrives with an excavator at precisely that tree, you are allowed to ask a few questions.

The provenance problem

This is where AI mathematics gets philosophically ugly very quickly.

Suppose a human mathematician proves a theorem. There is usually some intellectual genealogy:

A \to B \to C \to newtheorem .

Maybe the mathematician read paper $A$ , learned a technique from $B$ , generalized lemma $C$ , and then had some genuinely new idea.

The citations will not perfectly reconstruct the causal history of the proof, because human brains are not Git repositories, but at least there is a social system for trying.

Now replace the mathematician with a model trained on an enormous corpus, improved using enormous amounts of interaction data, surrounded by thousands of agents generating and consuming hundreds of billions of tokens.

What exactly is the provenance graph?

Something more like

{D_{1}, D_{2}, \dots, D_{N}} \overset{training}{\to} θ \overset{300B tokens}{\to} P .

Here $D_{i}$ might be papers, books, code, proofs, conversations, feedback, synthetic data or outputs derived from other models.

$θ$ is a few hundred billion parameters nobody can interrogate in the way we interrogate a bibliography.

And $P$ is the proof.

Now ask:

where did the idea come from?

Good luck.

This is definitely not merely a copyright problem or a corporate policy problem. Its a huge epistemological problem.

The machine can potentially produce a novel derivation without being capable of giving us a reliable causal history of why it searched that region of idea-space in the first place. And mathematical priority is largely about exactly that history.

Who saw the path first?

Who supplied the key lemma?

Who recognized that the forcing term was the right attack?

Who closed the final gap?

Those questions become very difficult when one participant in the collaboration is an enormous lossy compression of human intellectual history that can perform a few hundred billion additional acts of mathematical autocomplete before lunch.

And then everyone behaved completely normally

Buckmaster apparently contacted OpenAI because he had heard that OpenAI had heard about his and his collaborator's progress. He wanted to clarify that the rumors were confused and that their results would be published shortly.

There was another complication. His collaborator worked at Anthropic. OpenAI competes with Anthropic.

So Buckmaster emphasized that their work was personal rather than an institutional Anthropic project. They had apparently paid for the AI tools used in the research themselves, including a substantial OpenAI bill.

This did not make things simpler. It made things considerably stupider though.

According to Buckmaster's account, OpenAI researcher Sébastien Bubeck proposed possible ways to coordinate publication. One possibility was for the mathematicians to publish their result and OpenAI to publish its result the following day.

Another involved Buckmaster working with OpenAI on the Navier-Stokes proof while his Anthropic-employed collaborator was excluded from that particular paper.

Buckmaster declined.

Then the conversation apparently produced the sentence:

"Why would you ruin your career?"

Which is an absolutely phenomenal sentence to somehow emerge from a discussion about partial differential equations.

There was then another message along the lines of:

"If you don't want to be nice, then I don't have to be nice."

And a separate attempt to speak privately with the collaborator because Buckmaster might not have been "fully rational."

Remember where we started.

\nabla \cdot 𝐮 = 0 .

We are now threatening careers. Mathematics remains undefeated.

There are actually two different problems here

The interpersonal drama is entertaining, but I think it obscures two questions that should be separated.

The first is mathematical:

Is the proof correct?

The second is historical:

Where did the proof come from?

These are completely different questions.

A proof can be correct even if its provenance is horrible. A proof can also have immaculate provenance and be wrong.

Mathematics traditionally cares about both, but for different reasons. Correctness determines whether the theorem enters mathematics. Attribution determines how the humans who produced the mathematics are treated.

AI attacks the second problem much harder than the first. Because, in principle, formal mathematics gives us a remarkably clean way to attack correctness.

Lean does not care about vibes

OpenAI reportedly released both a conventional write-up and a formalization in Lean.

Lean is a proof assistant. At a very simplified level, you give it definitions, axioms and a proposed sequence of logically valid transformations, and it checks whether the conclusion actually follows.

Think of a theorem as

A_{1}, A_{2}, \dots, A_{n} ⊢ T .

A conventional proof is a human-readable argument that $T$ follows from the assumptions. A formal proof turns essentially every logical step into something the proof checker can verify.

So instead of:

Clearly, by the standard argument, the result follows.

Lean responds approximately:

No. Show me.

This is an excellent personality for a machine.

If the formalization is valid and accurately represents the intended mathematical statement, then we have an unusually strong form of verification.

But that second clause matters. A proof assistant verifies the theorem you actually formalized. It does not reach through the monitor and determine whether the theorem in your head was the same theorem you encoded.

If the intended problem is

P

but your formalization accidentally represents

P^{'},

Lean can establish

⊢ P^{'}

with absolute confidence while telling us nothing about

P .

The kernel checks the derivation. Humans still have to check the specification. This is software verification all over again. The program can perfectly satisfy the spec.

Unfortunately the spec was wrong.

Proof has two layers now

I think this distinction becomes increasingly important as AI starts producing serious mathematics.

There is derivational correctness:

A ⊢ T .

Did the conclusion logically follow from the formal assumptions?

Then there is semantic correctness:

T_{formal} \stackrel ? = T_{intended} .

Did we formalize the thing we actually meant to prove?

Proof assistants can make the first layer extraordinarily robust. They do not eliminate the second.

So "Lean verified it" should massively increase confidence, but it is not identical to "the Millennium Prize problem has definitely been solved."

The formalization itself needs expert inspection. The definitions need inspection. The correspondence with the Clay statement needs inspection. And, because this is mathematics, everyone will presumably inspect it until the Sun runs out of hydrogen.

Good. That is what should happen.

The strangest part is the search

The part I find more interesting than the corporate drama is the scale of the search. Three hundred billion output tokens in 88 hours. Forget Navier-Stokes for a moment.

What exactly is this thing doing to mathematics?

A human mathematician might spend years developing intuition about a problem. They read papers. Try a lemma. Fail. Notice why it failed. Invent a different formulation. Spend three months discovering that a minus sign has personally declared war on them. Talk to another mathematician. Abandon the approach. Come back six months later.

There is a sequential intellectual history to the search. An AI system can instead instantiate thousands of partially independent search processes.

Very crudely, if agent $i$ explores trajectory

𝒯_{i} = (x_{i, 0}, x_{i, 1}, \dots, x_{i, k}),

then thousands of agents can search

𝒯_{1}, 𝒯_{2}, \dots, 𝒯_{N}

in parallel.

Most trajectories die. Some produce intermediate lemmas. Those lemmas can be fed into other trajectories. Promising branches receive more compute. The resulting object starts looking less like one mathematician thinking very quickly and more like an industrialized evolutionary search over proof space.

Generate → Test → Kill → Fork → Combine → Repeat.

candidate ideas \overset{critic}{\to} survivors \overset{expansion}{\to} new candidate ideas .

Do this a few million times.

The weird thing is that mathematics is unusually compatible with this. Because at the end of the search there exists something close to an objective function. The proof either checks or it doesn't.

Lean (P) = {\begin{matrix} 1, & valid \\ 0, & invalid \end{matrix}

Reality has supplied a verifier. This is an enormous advantage.

Mathematics might be the perfect AI science

A lot of scientific work does not have this property. Suppose an AI proposes a new rocket engine. Wonderful. Now somebody has to manufacture it. The turbopump has to spin. The chamber has to survive. The injector has to not turn combustion instability into an extremely expensive percussion instrument.

Eventually reality evaluates the proposal:

design \to hardware \to test .

That loop takes money and time.

Mathematics is different. The artifact is the proof. And if the proof is formalized, verification can happen computationally. So the loop becomes

conjecture \to proof search \to formalization \to verification .

All four stages can, at least in principle, run on silicon.

This means mathematics may be one of the first serious intellectual disciplines where the entire research loop can be closed inside a datacenter. That should probably concern mathematicians slightly more than whether a chatbot can solve Putnam questions.

The interesting threshold is not

AI can answer math questions .

It is

AI can generate new mathematics \to AI can verify new mathematics \to AI can use that mathematics to generate more mathematics .

Once the loop closes, the relevant variable becomes iteration speed.

And computers are somewhat good at iteration speed.

But what counts as discovery?

Suppose the OpenAI proof is correct. Suppose also, for the sake of argument, that no private research from Buckmaster or his collaborator influenced the model in any way.

Who solved Navier-Stokes? "The model" feels incomplete. The model did not wake up one morning worried about fluid regularity. OpenAI chose the problem. Researchers designed the system. Other mathematicians produced essentially all of the mathematical literature it learned from. Thousands of agents performed the search. Humans presumably selected, inspected, formalized and presented the result.

Maybe the cleanest representation is not

person \to proof .

Maybe it is

civilization + model + compute + search procedure \to proof .

Which is less satisfying if you are trying to engrave one person's name onto a medal. But perhaps more accurate.

Scientific discovery has always been distributed. Newton had Hooke. Einstein had the mathematical machinery developed by Riemann, Ricci and Levi-Civita. Semiconductor fabs contain the accumulated work of millions of people nobody operating the scanner could individually reconstruct.

AI makes that dependence impossible to ignore because it compresses the dependency graph into one machine.

You ask the machine a question. It answers. And suddenly the entire intellectual supply chain disappears behind an API call.

Credit is not cosmetic

It is tempting to say none of this matters. Who cares who gets credit? We know something new about Navier-Stokes. Science advances. Next problem.

I don't think that works however. Credit is part of the incentive system that produces mathematics in the first place.

A mathematician might spend ten years on a problem with very little financial reward because the reward function contains other terms:

U = α (curiosity) + β (recognition) + γ (priority) + δ (career) + ε (money) .

For many mathematicians,

ε

is not exactly carrying the equation.

Remove recognition and priority and you have changed the incentive structure. This doesn't mean humans deserve ceremonial ownership of every theorem forever. It means that if AI systems depend on human mathematical work while making the causal contribution of particular humans increasingly difficult to observe, then attribution becomes an infrastructure problem.

We need provenance systems that are much better than:

the model says it came up with it.

The model does not know. That is sort of the problem.

The million dollars is almost irrelevant

Some people apparently framed the dispute around the Millennium Prize money.

That seems silly to me.

OpenAI reportedly spent something like $22.5 million in compute to pursue a theorem carrying a $1 million prize. This is not a profitable bounty-hunting strategy. And OpenAI has said it does not intend to claim the Millennium Prize. The actual prize is capability.

If a system can take a problem that resisted the mathematical community for a century and make decisive progress in

88 hours,

then the economically important output is not

$ 1, 000, 000 .

It is the existence of the machine. The proof is the benchmark result. Navier-Stokes is the eval.

That is a much bigger claim.

So did AI solve Navier-Stokes?

Maybe.

That is the boring but correct answer right now. There is a claimed proof. There is reportedly a Lean formalization. That is very serious evidence.

But the formal statement has to be checked against the intended Millennium problem. Experts need to inspect the argument. The Clay Mathematics Institute has a deliberately slow process for evaluating these things.

This is how mathematics is supposed to work.

A press release is not a theorem, and a theorem is not established because everyone involved has a lot of GPUs. And Lean verifying a formal statement is enormously important without making human semantic review obsolete.

So I would separate three claims:

The model produced a formal proof.

The formal proof is correct.

The formal theorem solves the intended Millennium problem.

These are related. They are not identical.

And then, entirely separately:

Who deserves credit?

That may end up being the harder question.

Part I aged badly

A month ago I ended an essay about Navier-Stokes with:

We went looking for the equation of water.

We found it.

Now we have to figure out what the equation knows.

Apparently the answer may have been sitting inside a datacenter.

Which creates a much stranger problem. For most of mathematical history, the bottleneck was obtaining the proof. Now imagine proof generation becomes cheap enough that machines can explore enormous regions of mathematical possibility, formalize what they find and verify the results themselves.

Then the bottleneck moves.

From:

Can we prove it?

to:

What should we ask?

and

Why is this theorem interesting?

and perhaps most annoyingly,

Where did the idea come from?

That is a very different mathematics. The funny thing is that Navier-Stokes itself already gave us the warning. Simple local rules can generate behavior far richer than anyone looking at the rules would expect.

simple rule + enough iteration \to unexpected structure .

In Part I, the rule was

\frac{\partial 𝐮}{\partial t} + (𝐮 \cdot \nabla) 𝐮 = - \frac{1}{ρ} \nabla p + ν \nabla^{2} 𝐮 .

Give it enough space and time and perhaps you get turbulence, energy cascades, singularities, maybe even structures capable of computation.

In Part II, the rule is a neural network.

Give it enough agents, enough tokens and $22.5 million of compute.

Apparently you might get a solution to Navier-Stokes.

I am beginning to suspect the dangerous term in every equation is iteration.