The Hand
In the
Water

Just before midnight on Monday, a mathematician at New York University hit post.

Tristan Buckmaster had spent months on a problem worth a million dollars. He had used OpenAI's coding tool the whole time. On Saturday, OpenAI announced it had finished the job.

What he wrote that night is the second most interesting thing about this story.

The first is that almost nobody who reported it told you which problem was solved.

The Navier–Stokes equations describe how fluids move. They are the reason a weather model works at all, and the reason turbulence is still the last open wound in classical physics. In 2000 the Clay Mathematics Institute put a million dollars on one question about them and made it one of seven Millennium Prize Problems.

Ninety years ago, Jean Leray proved something unsettling. He showed that solutions to these equations always exist in a weak sense, and then admitted he could not rule out that they tear themselves apart. Nobody has closed that gap since.

On Tuesday the world was told a machine closed it in eighty-eight hours.

That is not what happened. What happened is more interesting, and it turns entirely on a single word that no headline had room for.

A forcing term is a hand.

It is an outside push applied to the fluid at every point, smooth, and in this case switched off outside a small patch of space and a short window of time. Stir a cup of coffee and your spoon is a forcing term.

OpenAI's theorem builds one very particular push. Under that push, in finite time, the speed of the fluid runs away to infinity while its total energy stays bounded. The water tears. The hand is what tore it.

Door A asks whether water tears itself. Door C asks whether water can be torn.

That is the whole story, and it is the one thing a headline cannot fit.

In two dimensions, water behaves. In three, it might not, and the difference has a name. A spinning tube of fluid in three dimensions can be pulled thin. Pull it thin and it spins faster, the way a skater pulls in her arms. Faster spin pulls harder. It feeds itself. Two dimensions forbid the move entirely.

In 2014 Terence Tao built a fake Navier–Stokes, close enough to the real one to share its energy budget, and proved the fake one blows up. The point was never the fake equation. The point was that any proof leaning on the energy budget alone is dead on arrival, because a doomed equation passes the identical test.

He called it the supercriticality barrier. It is the wall every serious attempt has hit.

Three hundred and forty one thousand lines of Lean 4 sit on GitHub. They compile. The machine agrees the argument is valid.

Here is the part every engineer already knows in their bones. A proof assistant returns exactly one bit. It tells you the theorem follows from the assumptions you wrote down. It does not tell you that the theorem you wrote down is the theorem you meant.

The tests pass. Nobody has published a review of the spec.

Somebody credible has to read the formal statement, line by line, and confirm it encodes Fefferman's door C and not a cousin of it. As of this writing no named expert in partial differential equations or in Lean has put their name to that confirmation in public.

This is not a reason to assume the proof is wrong. It is a reason to notice that the loudest evidence being waved around, the green compile, is evidence for a narrower claim than the one being celebrated.

Anthropic hit a version of the same wall four days earlier and handled it differently. Its model produced a machine-checked Fermat's Last Theorem, thirteen million lines of Lean, and Kevin Buzzard at Imperial College went on the record about what it did and did not establish. A named human vouched for the statement. That step is the whole ballgame and it has not happened here yet.

In 2014 the Kazakh mathematician Mukhtarbay Otelbaev announced he had solved Navier–Stokes. Serious people took it seriously. Then he emailed Stephen Montgomery-Smith.

Grigori Perelman posted his Poincaré proof in 2002. It was right. Three separate teams then spent years writing out the verification so the field could check it, and Clay paid in 2010.

Eight years, for a proof that was correct the day it appeared.

Clay's own rules require refereed publication, then a two year wait, then general acceptance by the mathematical community. Run that clock from a paper that has not been submitted anywhere.

Terence Tao has not assessed OpenAI's manuscript. He praised different work, by other people, and said clearly that it had not reached Navier–Stokes. If you saw his name attached to an endorsement this week, you saw a misreading.

What he did say is the part that should keep the builders awake.

Sit with what OpenAI volunteered about its own timeline. The trigger was not a paper. It was not a public preprint. It was a rumour that somebody was close.

Run that forward. If saying out loud what you are working on summons ten thousand agents to get there first, the rational move is to stop saying it. Open science runs on the exact opposite habit, and it has run on it for four hundred years.