OpenAI published an AI-generated solution to the Navier–Stokes millennium problem, with a writeup and a formal proof in Lean: On the Navier–Stokes Millennium Prize Problem. The coverage from Latent Space reports that the result came out of a run of around 10,000 agents collaborating, with enormous time and compute figures. And there's already a dispute: an NYU mathematician accuses OpenAI of fighting dirty over a career-making problem, according to TechCrunch.
Why it matters
The headline is the math. The signal is something else: the proof is in Lean. That means the result doesn't depend on us trusting the model. A deterministic verifier checks it, and that ends the argument about whether the output hallucinated or not.
That's the part I care about as a dev, and it's the part almost nobody is looking at. For two years the debate was "do I trust what it generates for me?". Here the debate disappears, because there's an external oracle that says yes or no. The model generates, the verifier judges. No opinion in between.
The other half of the signal is uncomfortable: according to what Latent Space reported, this was achieved by throwing an amount of parallel compute at it that none of us will ever have. It wasn't a smarter model solving the problem in one shot. It was a brutal number of attempts, organized by the agents themselves, against a judge that filters. That's not magic: it's search at scale with cheap verification.
What changes in practice
The pattern can be copied without having 10,000 agents. The question to ask before delegating a task to a model is now a single one: do I have an automated verifier for this?
If the answer is yes, you can crank up the aggressiveness of your delegation enormously, because the cost of a failed attempt is zero: the machine discards it, not you reading a diff. If the answer is no, you're still the bottleneck, and all the speed you gain generating you lose reviewing.
┌──────────────┐ generates ┌──────────────┐
│ Model │ ──────────► │ Candidate │
└──────────────┘ └──────┬───────┘
▲ │
│ retries ▼
│ ┌──────────────┐
└───────── no ────────│ Verifier │
└──────┬───────┘
│ yes
▼
┌──────────────┐
│ Human │
│ review │
└──────────────┘The verifier doesn't have to be Lean. In a real project you already have it at hand, and you're probably wasting it:
- The compiler. TypeScript in strict mode rejects a huge amount of invalid output before you ever read it.
- The test suite, when you wrote the tests yourself and they weren't generated by the same model that writes the implementation.
- Property-based tests, which are the closest thing to a formal proof you'll get without switching languages.
- The linter, the typechecker, and schema validation at the edges.
The architectural consequence is direct: investing in verifiability pays off more than investing in prompts. Strong typing, explicit contracts at the system boundaries, and deterministic tests aren't just hygiene: they're what makes serious delegation possible.
When NOT to use it
Here's the honest part, because this week's enthusiasm is going to do a lot of damage.
| Situation | Delegate at volume? | Why |
|---|---|---|
| Refactor with solid pre-existing tests | Yes | The verifier is real and it's yours |
| New feature without a clear spec | No | There's nothing to verify against |
| Tests generated by the same model | No | The judge and the defendant are the same person |
| Product or UX decisions | No | No automated verifier exists |
| Code with irreversible external effects | No | A failed attempt doesn't cost zero |
Three concrete limits:
Cost is not a detail. Latent Space reports a run with thousands of agents and a compute figure that puts this far beyond any normal team's budget. Porting that strategy into a sprint without measuring spend is the fastest way to burn money. The pattern copies; the scale doesn't.
Without a verifier, parallelism makes things worse. Ten candidates with no automated judge aren't ten chances to get it right: they're ten things you have to read. Massive search only pays off when filtering is cheaper than generating.
The authorship dispute isn't noise. The TechCrunch article describes a conflict over a problem that defines careers. Translated to our world: when the output of an automated system lands in a shared repo, the question of who answers for that code stops being philosophical. If your team doesn't have an answer to that yet, don't work it out after the incident.
And something the available material doesn't let us claim: there's no confirmation that the mathematical community has accepted the result, nor that the prize has been awarded. Verification in Lean is strong, but acceptance of a result of this caliber takes time. Anyone telling you today that the problem is closed is moving faster than the available evidence.
What I'd do today
Nothing dramatic. What I would do is a half-hour audit of the project I'm on: where I have real automated verification and where I'm pretending I have it. That map tells you exactly what you can delegate tomorrow and what you can't.
And wherever it's missing, I'd invest there before anything else AI-related. Stricter types, contracts at the edges, tests that don't depend on chance. Not because they're fashionable, but because they're the only infrastructure that turns a model into something that works for you instead of giving you work.
The rest —the 10,000 agents, the 88 hours, the million dollars— is theirs. The lesson is ours, and it's a good deal more boring: whoever has the better verifier wins.