What OpenAI Actually Did to Navier-Stokes

OpenAI says a team of its AI agents has settled the Navier-Stokes Millennium Prize problem, one of the seven problems the Clay Mathematics Institute put a million dollars on in 2000. The reported numbers: about 10,000 agents working together for about 88 hours, a 166-page paper, and a proof written out in Lean, a language a computer can check line by line. Scientific American's headline asked whether they solved the wrong problem.

I wanted to see for myself. The Lean is public on GitHub, so I read it, rebuilt the idea in pieces the engine behind this blog can test, and then asked the question I actually care about: if you build something that moves through water or air, does any of this matter?

Short version: they did prove something real, and it is not the thing most people mean when they talk about this problem. You can make a fluid blow up in a simulation, but only if you hand it the blowup. And in a real fluid the mathematics never gets that far, because the water boils first.

What the prize actually asks

The Navier-Stokes equations describe how fluids move: water in a pipe, air over a wing, smoke off a candle. The open question is whether a smooth flow can ever tear itself apart. Could the speed at some point become infinite in a finite time, with nothing pushing on the fluid from outside?

Clay's official statement allows four ways to win. Two prove the flow always stays smooth, one for all of space and one for a box that wraps around. The other two prove the opposite: that some smooth start and some smooth outside force lead to a breakdown. Those are options (C) and (D), and they are what OpenAI proved. Their two Lean theorems are literally named navier_stokes_breakdown_R3 and navier_stokes_breakdown_periodic.

The force is the whole story, so here is how they used it.

The recipe, read from their Lean

1. Start with the fluid at rest. The initial velocity is zero.
2. Pick the answer first. They wrote down a spinning, collapsing vortex that blows up at time t = 1. Its core gets thinner like (1 − t)^1/2, shorter like (1 − t)^{1/2 − h}, and spins faster like (1 − t)^{−(1/2 + h)}, for a constant h between 0 and a half.
3. Define the force as whatever makes that true. Put the chosen flow into the Navier-Stokes equations and see what does not balance. That leftover is the force. By construction, the chosen flow is then a solution.
4. Prove the force is allowed. This is the hard part, and it is where the 166 pages go. Clay requires the force to stay smooth and to fade away at large distances, forever, including through the moment of blowup. A force that itself blows up would be cheating. They show theirs does not. The vortex is switched on smoothly from rest, and from t = 7/8 the force is handed over to a separately built smooth force that matches the leftover right up to the blowup and carries on smoothly past it. The flow's energy stays finite throughout.

That is a legitimate reading of the problem as Clay wrote it, and the formal proof is a real achievement. It is also why the reaction has been mixed. Luis Silvestre at the University of Chicago put it most cleanly: "The Clay problem is settled, but the main problem for the Navier-Stokes equations is not." The question physicists care about is whether a fluid left alone can blow up, with no designed force. That one is untouched. Stan Palasek at Princeton, in an exchange with Terence Tao, pointed out an obstacle to extending this approach to the unforced case: viscosity drains energy faster than this growth mechanism can build it. There is also a public dispute about who deserves credit for the underlying ideas, which I will leave to the people involved.

What I checked, and what I did not

I did not compile their proof. Building 640,000 lines of Lean against Mathlib is a job for a machine with more patience than this one. What I did was a static scan of every file.

640,857 lines in 2,655 files, and no sorry, admit, new axiom, native_decide or unsafe anywhere outside the five blanks the challenge statement leaves on purpose. Those five words are the ways a Lean proof can quietly skip a step, so their absence is a good sign. It is not a verification. A scan tells you nobody skipped a step in the text. Only the compiler tells you the steps are right.

Rebuilding it in three pieces

Nothing on this site solves the Navier-Stokes equations in three dimensions, and I did not try to reproduce 166 pages. What I could do is rebuild the logic in pieces small enough to check exactly, which is how this engine does everything: every number is computed two ways that share no algebra, and the two have to agree.

Piece one: the obvious design fails

The first thing anyone would try: take a flow you already know blows up, and add whatever force makes a real, viscous fluid follow it. The simplest such flow is a wave that steepens until it breaks, from Burgers' equation, a one-dimensional cousin of Navier-Stokes.

The force you need grows like (1 − t)^−5/2. The engine measures the exponent at −2.498 against a predicted −2.5. Ten times closer to the breaking point takes about 315 times the force. A force that blows up is exactly what Clay forbids, so this naive design is disqualified. The 166 pages exist to find a collapsing flow whose leftover force stays tame.

Piece two: a real blowup, put in by hand

Here is a flow that genuinely solves the Navier-Stokes equations with no force at all, and still blows up. Take a spinning vortex and squeeze it with a strain, a flow that pushes in from the sides and stretches it along its axis. If the strain grows like 1.5/(1 − t), the vortex has an exact closed-form solution, and the engine checks it satisfies the equations to nine parts in a billion.

On the left, the core shrinks like (1 − t)^1/2, the same radial rate as OpenAI's vortex, and its spin blows up. On the right, the strain is held steady and the core heads for a fixed radius of 0.1633, which is √(4ν/α) exactly: the Burgers vortex, which has been known since 1948.

So why is this not a prize-winning blowup? Because the vortex blows up only because the strain does. The strain field grows with distance, so it has infinite energy, and its rate is itself infinite at t = 1. The singularity arrives from outside, which is the same move as the designed force, made in a different place.

Piece three: their coordinates

OpenAI's vortex lives in a set of coordinates that squeeze space unevenly as the blowup approaches. I transcribed their definitions directly from their Lean files and checked them against the identities those files state. The defining equation holds to three parts in 10¹⁶, which is the precision of the arithmetic itself.

The core thins faster than it shortens. Its radius goes like (1 − t)^1/2 and its length like (1 − t)^{1/2 − h}, so it collapses into spaghetti. The engine measures both exponents exactly. The figure uses h = 0.25 so the stretching is visible in a few seconds. It draws their coordinate region, not their velocity field, which I have not rebuilt.

What this means if you build things

This is where it gets useful. The mathematical blowup needs the core to shrink to zero size. A real fluid stops being the fluid in the equations long before that. Three things give way as a vortex core shrinks, and the one with the biggest threshold goes first:

• Cavitation. A vortex holds itself together with low pressure at its centre. Squeeze the core and the pressure drops further. In water, when it reaches the vapour pressure, the water boils in the core. That is tip-vortex cavitation, the reason ship propellers pit and erode.
• Compressibility. The swirl speeds up as the core shrinks. Past about a third of the speed of sound, the equations for an incompressible fluid are the wrong equations.
• The continuum. Navier-Stokes treats fluid as smooth stuff. When the core is only about a hundred molecules across, it is not.

I ran the strained vortex from piece two in real water and real air at 20 °C, with a circulation of 1 m²/s and a core that starts 50 mm across, and let the engine report what breaks first.

• In water, it boils first, when the core is 13.3 mm across, 171 milliseconds before the mathematical blowup. The compressibility limit is at 0.23 mm and the continuum limit at 31 nanometres, so neither ever gets a look in.
• In air, it goes compressible first, at 0.99 mm, 3.68 milliseconds before the blowup. The continuum limit is down at 6.5 micrometres.
• Hold the strain steady and the air vortex never breaks. It settles at 6.34 mm, above every limit. The water one still boils, 1.77 seconds in, because a steady vortex of that strength already has enough low pressure at its centre.

That last pair is the design lesson. The singularity is never your problem, because the fluid gives out first. The limits are the problem, and they are designable. Every limit radius grows in proportion to the circulation, so a vortex half as strong cavitates at half the radius. A weak vortex, 0.05 m²/s in the widget below, held at a steady strain, settles at 1.64 mm against a cavitation line at 0.67 mm and never boils. Spread the lift along the blade, stop the tip from concentrating it, and never let the strain run away. That is what propeller and wingtip designers already do, and now you can watch why.

So how do you trigger it in a simulation?

You put it in by hand. That is the honest answer, and it is also what OpenAI did, in a far more sophisticated way. There are two doors:

1. Design a force that pushes the flow into the collapse, as in pieces one and three.
2. Impose a strain that is itself infinite, as in piece two.

Either way, the singularity is something you supplied. The engine has a module for exactly this now, and it follows the same rule as everything else here. It will build you the collapse, tell you the force or strain it took, and then tell you which real limit your fluid hits first. It will not report a blowup in water, because water does not have one.

Try it

Run the clock and watch the core fall down the ladder. The ladder is logarithmic, because the core goes from 50 mm to a few nanometres. Then hold the strain steady, switch to air, or turn the spin down until nothing breaks.

The numbers past the first line are what the equations say, not what the fluid does. In water that includes a core pressure that goes negative and keeps going, to two thousand atmospheres below zero with a millisecond left, which no liquid holds. The equations will keep returning a smooth, well formed answer long after the fluid they describe has boiled. This blog keeps finding that shape: a model that answers a question its own assumptions stopped covering.

The bigger claim in the same repository

The Navier-Stokes result gets the headlines because it has a prize attached. The other half of the repository may matter more. It claims a blowup in the Euler equations, which are Navier-Stokes with the friction taken out, and it claims it with no force at all. I went back and read that statement too.

Here is what their Lean says, in plain terms:

• The fluid starts smooth, and all of its motion is inside a bounded region, with the fluid still everywhere else. There are no walls: the fluid fills all of space. Its energy is finite.
• Nothing pushes on it. No force and no viscosity. The fluid is left entirely alone.
• It flows smoothly up to some time no later than t = 1. At that time the velocity's gradient becomes infinite. They also prove the stronger test the field uses to certify that a blowup is real and not a quirk of how it is measured: the total spin over time, the Beale-Kato-Majda integral, diverges.
• The construction is completely different from the Navier-Stokes one. The starting flow is the limit of an infinite family of "packets" at smaller and smaller scales, set off one after another, each with a shorter time to live than the last.

For context, the closest earlier results needed a wall for the fluid to press against (Chen and Hou's computer-assisted proof), or a starting flow that is not fully smooth (Elgindi). A smooth, finite-energy blowup in open space with nothing forcing it would be a first. If it holds, it is a bigger result than the one that got the headlines.

It still does not settle Navier-Stokes. The one thing Euler leaves out is viscosity, and viscosity is exactly what Palasek's obstacle is about. A mechanism that works in a frictionless fluid can be smothered by friction.

What is still open

• The unforced Navier-Stokes problem. Does a real, viscous fluid left alone ever blow up? Nobody knows, and neither result here says.
• Whether the Euler proof holds. It is 1,839 Lean files and has been public for two weeks. The mathematical community has not had time to digest it, and a machine-checked proof is only as good as the statement it checks, which is why I have quoted the statement rather than the headline.
• My own limits. The reported facts about 10,000 agents, 88 hours and 166 pages, and the quotes from Silvestre and Palasek, agree across several independent reports, but this network cannot open OpenAI's pages or Scientific American's directly, so I have read them second-hand. The Mach and continuum lines are conventional engineering thresholds, not cliffs, and the engine says so every time it uses them.