OpenAI published on Tuesday that an internal model — not one you can call — had produced a finite-time blowup for the three-dimensional Navier–Stokes equations. Roughly 10,000 agents running concurrently, 88 hours of wall clock between 1 and 5 September, 2.7 million messages, somewhere around 130 billion output tokens.

Then the whole thing got formalised in Lean and machine-checked in another seventeen hours.

And by the time most people had finished reading the announcement, the story had stopped being about fluids.

What the theorem actually says

Navier–Stokes describes how a fluid moves. The Millennium question is whether a fluid that starts out smooth stays smooth forever, or whether the equations can eat themselves — some quantity running off to infinity at a point in finite time. That's a blowup, and it's the difference between "this model is always physically meaningful" and "this model has a hole in it we've never found".

Charles Fefferman's official problem statement is four claims, not one. (A) and (B) say solutions stay smooth forever, on all of space and on the periodic torus respectively, with no external force at all. (C) and (D) are the breakdown versions, and there the statement permits a smooth, well-behaved external force. Prove or disprove any of the four and the problem is resolved.

OpenAI proved (C) and (D). Roughly a hundred pages, starting from a fluid at rest, with a smooth force applied to it, finite energy throughout, and a singularity anyway.

So by the letter of the rulebook: yes, that's a resolution. I want to be fair about this because the internet has spent two days being unfair in both directions at once.

But when a mathematician says the Navier–Stokes problem out loud, they are picturing (A) or (B). No hand on the scale. Being allowed to keep pushing the fluid for the entire run is help, even if the pushing has to stay smooth and finite-energy. It's the difference between showing your service falls over under its own steady load and showing it falls over if you're also allowed to keep inventing new traffic while it runs. Both are real failures. Only one of them tells you the thing is broken on its own.

The force is the asterisk. It's a legitimate result and it's in the official rulebook, and it is also not the version anybody has spent ninety years failing to prove.

Seventeen hours

Here's the part getting maybe a tenth of the attention it deserves.

A hundred-page proof of something this size normally means a year or two of referees. Seminars. Somebody finding a gap on page 61 in month nine. Perelman's Poincaré work needed people to write entire expository volumes just to check it, and that took years.

This one came with a Lean formalisation and a kernel that agreed with it. That's not "the reviewers found it convincing". It's the same kind of true as your build passing — a machine mechanically walked every step down to the axioms and didn't complain.

The historically expensive step, is this correct, dropped to a rounding error. Seventeen hours. Every other step in the process stayed exactly as expensive as it was the week before.

And we know this shape. It's every repo where CI got fast and PRs still sit for three weeks, because the argument was never about whether the tests pass. It was about ownership, and scope, and who gets to say yes. Make the machine-checkable half free and you don't delete the bottleneck. You just find out what the bottleneck actually was.

Here it turned out to be the author list.

The part the kernel can't check

Tristan Buckmaster at NYU and Levent Alpöge — Harvard mathematician, now on Anthropic's technical staff — had been working this family of equations for about a year, with Claude, Codex and Astra. On 7 September they published three blowup results: incompressible porous media, Boussinesq, and three-dimensional incompressible Euler, which is the zero-viscosity cousin of the real problem. With Lean formalisations, as it happens.

OpenAI's run started on 1 September, after rumours that those two had something. OpenAI says it reached out to offer a concurrent release recognising their priority.

Buckmaster tells it differently. He says Sébastien Bubeck offered him a choice: publish the partial result and let OpenAI announce the full one, or publish and claim the prize himself — on condition that he confirm OpenAI's model had also solved it, and that he take Alpöge's name off the paper, because of the Anthropic affiliation. Buckmaster says he refused and was asked why he would want to ruin his career. OpenAI denies touching any private work or Codex logs.

I don't know what was said on those calls and neither do you, and priority disputes are as old as mathematics. They're usually boring. Two people got somewhere at nearly the same time, the record sorts it out, everyone is mildly annoyed for a decade.

The affiliation clause is the bit I can't walk past, and it's the one part of the allegation that has nothing to do with who was first. An author list is not a sponsorship banner. It's the record of who did the work — and it is, conveniently, the single artifact in this entire story that no Lean kernel will ever verify for us. Asking for a name to come off it because of where that person collects a paycheque is a different category of request from "please cite us too", and treating the two as negotiable against each other is how you end up with a literature nobody trusts.

Answers and understanding

Terence Tao called the Buckmaster–Alpöge work a remarkable achievement, and then said the line that's been rattling around my head since: there's been a very strange and unprecedented decoupling this year between getting answers and getting understanding.

That's precisely what a Lean-checked hundred-page proof is. You have a certificate that the statement is true. What you don't automatically have is the thing mathematics was for — somebody who can tell you why fluids do this, what the mechanism is, what else it implies. Those two used to arrive together, because the only way to get the certificate at all was for humans to understand it well enough to check it by hand. That coupling is gone. Nobody has decided what replaces it.

Meanwhile the Clay Institute has accepted nothing and still lists Navier–Stokes as unsolved. Its rules require a solution to sit in a peer-reviewed journal for two years and win general acceptance in the field before a prize committee is even convened. Martin Bridson's statement was that the evaluation process is deliberately unhurried and will be absolutely rigorous, which I like enormously. Deliberately unhurried is the correct posture for the institution whose entire job is to be the slow, boring, final word.

OpenAI says it won't claim the million anyway. Given the two-year clock that's a slightly cheaper gesture than it reads, but it's still the right call, and it takes the ugliest available incentive off the table.

What I'd take from it

Formal verification stopped being a curiosity this week. If you've had Lean and mathlib filed under interesting, academic, not my problem, a hundred pages of frontier analysis went from unreviewable to mechanically certain in under a day. That capability doesn't stay in pure maths. Protocol specs, consensus rules, crypto primitives — anything where "we reviewed it carefully" is currently the whole safety argument is now a candidate.

The broader one: when you automate the checkable half of a review, budget for the other half getting much louder. Everything that used to hide comfortably behind we still need to verify this — attribution, ownership, credit, who gets to announce — becomes the entire schedule the moment verification stops taking a year.

And a tiny practical one, because we're going to need it a lot. For the next few years, "an AI proved X" will mean anything from a Lean-checked theorem to a press release. Ask which exact statement. Ask whether there's a formalisation. Ask who else was already working on it. Three questions, and they'd have sorted out most of this week before it started.