On the Navier–Stokes Millennium Prize Problem by OpenAI:
We're sharing a solution to the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. This proof, produced by an internal OpenAI system, shows that the dynamics of the Navier-Stokes equations for fluid motion can develop a singularity in finite time. We're sharing both a writeup of the proof and a formalization in Lean.
The Clay Mathematics Institute has offered $1 million for this problem since 2000. It's a question about whether fluid flow, left alone, can ever spiral into infinite velocity on its own, one of seven Millennium Prize Problems, and the hardest kind of mathematics to describe.
OpenAI apparently put roughly 10,000 agents on the task, 88 hours of reasoning, 130 billion output tokens. Then spent another 17 hours to validate the result in Lean, a proof assistant that mechanically checks every logical step. Estimated compute cost: somewhere between $15 million and $22 million! That is at least fifteen times the prize itself.
OpenAI cannot even claim the money as the actual prize question is about fluid left completely alone, no outside energy added. What OpenAI proved is that if you keep pushing energy into the fluid from outside, you can eventually force a blowup (a singularity, infinite velocity). That's a real result, albeit not one that meets the challenge.
The interesting thing is that the output is essentially unreadable, even to the mathematicians qualified to check it, 2.3 million lines of Lean code, verified mechanically, but the strategy behind it is now too large for any one person to hold in their head without AI assistance. It's the same trade developers are making with AI-generated code that passes its test suite. Green checkmarks confirm the logic holds together somewhere, even if no human actually understands what the code does.
Let's review. $15 million in compute, at least fifteen times the prize. An answer to a different, easier question than the one Clay actually asked. 2.3 million lines of proof that nobody has finished reading. Ten thousand agents and 130 billion tokens. I feel the need to remind everyone that activity is not the same as impact.