10,000 Agents Are Easy. The Proof Is Hard.

This week OpenAI said an unreleased internal model had solved the Navier-Stokes Millennium Prize Problem, the 200-year-old question of whether smooth three-dimensional fluid motion can break down. According to the announcement, it can: there is a configuration where a vortex tightens and spins ever faster until the maths stops behaving. OpenAI published a 165-page proof and says it does not intend to claim the $1 million prize.

The maths will be argued about for months. What I can't stop thinking about is the machinery.

Ten thousand agents, eighty-eight hours

Work reportedly began on 1 September, after a rumour that another Millennium problem had fallen. The run took 88 hours and used as many as 10,000 agents working roughly concurrently.

Sit with that number. Almost every AI system any of us has touched this year is one agent, or a small crew with job titles: a researcher, a writer, a checker. Ten thousand agents running side by side for four days is not a bigger version of that. It's a different regime, closer to a compute cluster than to an assistant. It says the coordination problem and the cost problem have quietly been solved well enough to point a swarm at a wall and leave it running over a long weekend.

That's the headline. Here's the load-bearing part.

The proof is what makes the swarm usable

Alongside the 165 pages, OpenAI published a Lean formalization: the argument rewritten in a language a computer can check line by line, mechanically, with no opinion involved.

Without it, what do you actually have? A very long document produced by a model nobody outside the company can inspect, released by an organisation with every commercial incentive to overclaim, about a problem so hard that only a few hundred people on Earth can referee it. That is not a result. That is a press release with equations in it.

A 165-page proof from a model nobody can inspect is a claim. The same proof with a machine-checked formalization is an artifact. The verifier is what converts one into the other.

Mathematics is the rare field that has a total formal checker. Most of the world does not. And that, I think, explains the strangest pattern in this week's news: the same idea keeps surfacing in industries that have nothing to do with each other.

The same pattern, three more times

In marketing software. At its K:BOS conference on 9 September, Klaviyo opened its platform to outside AI systems: more than 260 Model Context Protocol tools and more than 490 APIs, reachable from Claude, ChatGPT or whatever agent a team already runs. An agent can now read the data, write to it, and put a campaign live without any human opening Klaviyo. Buried in that announcement is a small design decision worth more than the tool count: its preview of plain-language SQL returns the answer and the query that produced it. You get the number and the receipt. That's verification built into the interface.

In drone detection. The open-source counter-drone stack has fallen through the floor. A stereo drone tracker with two cameras, YOLOv11 detection, 3D triangulation and occlusion handling now runs on a roughly $550 Jetson build. The benchmark datasets are free. The simulators are free. An open 10.5 GHz phased-array radar design has been accepted for crowdfunding. So "we can detect drones in video" is no longer a business, it's a weekend project competing with a GitHub repository. What is still scarce is the evaluation: calibrated confidence that means what it says, honest performance on the genuinely hard cases (bird versus hobbyist versus news helicopter, at range, in haze), and a report a regulator or an insurer would accept. The detector is the commodity. The proof is the good.

In where the money goes. Over the twelve months to mid-2026, vertical AI agents took 30 of 59 disclosed agentic deals and $2.640 billion raised, about 51% of deal count and 56% of capital. The stated investor preference includes "vertical AI tools with measurable business results." That's the same test written as a cheque-signing criterion. Meanwhile Euno raised a $23M Series A on 9 September explicitly in the agent-context space, which tells you the plumbing layer under all this now has a name and a price.

What this means if you use AI at work

Generating output stopped being the bottleneck some time ago. Anyone can produce a plausible report, a campaign, a code change, a detection. The bottleneck is knowing whether it's right, and "a human reviews it" is not an answer, because at any real volume the human doesn't, and everybody involved knows it.

So the question to ask of every automated workflow is embarrassingly simple: what is the cheap, automatic check that proves this output is correct? Not a vibe. Not a spot check. An assertion that runs on every single execution and logs pass or fail. Did the tracking pixel actually fire. Do all the links resolve. Does the reported spend reconcile to the platform's own API to the cent. Is the field the agent claims to have filled actually populated.

Those checks are boring and usually about twenty lines of code. They're also the entire difference between an automation you trust and one that fails silently for six weeks while everyone assumes it's fine.

The honest caveat

This is a company announcement about a model nobody outside OpenAI can examine, and the mathematical community's verification of the Lean artifact is still in progress. Treat it as a strong signal about method, and hold the mathematical result loosely until independent mathematicians confirm the formalization compiles and says what it's claimed to say.

Which is, pleasingly, the whole point. Even here, the claim is only worth what the check is worth.