The Unread Proof

An internal OpenAI system produced a Lean-formalized proof that the Navier–Stokes equations can develop a finite-time singularity when energy is continuously forced into the fluid, a result OpenAI published alongside a 2.3-million-line Lean formalization. The proof does not resolve the Clay Mathematics Institute's Millennium Prize question, which since 2000 has offered $1 million for the case of fluid left completely alone with no outside energy added. OpenAI reportedly ran roughly 10,000 agents for 88 hours of reasoning and 130 billion output tokens, then spent 17 hours validating in Lean, at an estimated compute cost of $15 million to $22 million — at least fifteen times the prize.

On the Navier–Stokes Millennium Prize Problem https://openai.com/index/navier-stokes-solution/ 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 https://www.claymath.org/millennium/navier-stokes-equation/ 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 https://lean-lang.org/ , 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 https://tech.yahoo.com/ai/articles/openai-10-000-agent-navier-200053357.html . 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 https://www.poppastring.com/blog/ai-splits-the-market is not the same as impact.