OpenAI: ten thousand agents on a Navier-Stokes result

The system is described as coordinating agents running on an internal model, subdivided into groups, with agents able to communicate with others in their own group. The Navier-Stokes work involved on the order of ten thousand concurrent agents. The two structural details worth extracting are that the population was partitioned rather than flat, and that communication was scoped to the partition rather than global.

Both of those are the obvious engineering answer to the obvious problem, which is that a flat population of ten thousand communicating peers is not a system, it is a broadcast storm.

Communication cost between n participants who can all talk to each other grows with the square of n, so ten thousand peers is on the order of fifty million possible channels and no useful signal in any of them. Partitioning into groups makes the cost linear in the number of groups and quadratic only within one, which is the same argument as sharding, and the same argument as a service mesh preferring a hierarchy to a full graph.

Cross-group communication then needs a deliberate mechanism, and the account names one: Codex was used to consolidate promising intermediate ideas from different groups. That is a reduce step. Groups explore independently, something reads across them and pulls out what is worth propagating, and the result seeds further work. It is map-reduce with a language model as the reducer, and the shape is much older than the tooling.

There is an earlier phase reported that is more instructive than the headline, because it shows the resource allocation being managed rather than simply spent. Nearly a hundred agents worked for about fifty hours on the related Euler equations before resources were redirected. That is a bet placed, evaluated and abandoned, which is what a search over an expensive space has to look like: run cheap exploratory arms, decide, and concentrate the budget on the one that is moving.

The timeline gives the whole thing a scale. Training of the model began on 28 August, agents were launched on 1 September, and the result was reached on 5 September, about 88 hours after the first agents started. Then a further 17 hours of formalisation and checking. So the compute is enormous and the wall-clock is four days, which is the trade being demonstrated: an embarrassingly parallel search converts money into elapsed time at a rate no individual can match.

The reported figures are unusually specific and worth doing arithmetic on, because the arithmetic is where the intuition comes from. Across all of the mathematical problems attempted, the agents exchanged 4.9 million messages and generated roughly 300 billion output tokens. The Navier-Stokes work alone accounted for 2.7 million messages and approximately 130 billion output tokens. Divide those by the population and the picture sharpens considerably. Ten thousand agents and 2.7 million messages is about 270 messages per agent across the run. Ten thousand agents and 130 billion output tokens is about 13 million output tokens each. Over 88 hours that is roughly 150,000 output tokens per agent per hour, or on the order of 40 per second, sustained, per agent, for the better part of four days.

Two things follow from those numbers. The first is that this is not a chat workload, it is a batch compute workload that happens to be expressed in tokens, and it should be reasoned about the way any large batch job is: total throughput, cost per unit of work, and whether the result justified the spend. The second is that the message count is small relative to the token count, about 48,000 output tokens per message, which says the agents were producing substantial artefacts rather than conversing. That is the right shape. An agent population whose token budget goes into coordination rather than into work is a population doing very little.

The ratio between the two problems is also informative: Navier-Stokes took roughly 55 per cent of the messages and 43 per cent of the output tokens of the whole programme, so it was the largest single consumer but not the only one. That is what a portfolio looks like rather than a single bet, and it is consistent with the earlier arm being abandoned: several things were being tried and the accounting reflects it.

The honest caveat is that output tokens are not the cost. Input tokens are not reported, and in an agent system they usually dominate, because every step re-reads context, tool results and other agents' messages. A system generating 130 billion output tokens is plausibly reading many times that, which is why the public figure is a lower bound on the work rather than a measure of it. Anyone estimating the cost of something like this from the output count alone will be out by a large multiple, and the direction of the error is always the same.

The agents are described as having two capabilities beyond talking to each other: they could run code, and they could consult a cached version of the internet. Both choices are more interesting than they sound, and the second is the one worth pausing on.

Code execution is what makes a search over mathematics tractable rather than merely fluent. A conjecture can be tested numerically, a counterexample can be looked for by brute force, an algebraic manipulation can be checked by a computer algebra system, and a candidate construction can be simulated. That converts a large class of questions from things an agent asserts into things an agent finds out, and the difference in reliability between those two is the entire reason tool use exists.

A cached internet rather than a live one is a deliberate constraint and it buys three things at once. Reproducibility: ten thousand agents hitting live sources would each see a slightly different web, so the corpus would not be a fixed input and the run would not be repeatable. Rate limiting: ten thousand concurrent agents making live requests is a denial of service against whatever they are reading, and would be blocked within minutes. And determinism of the boundary: with a snapshot, the question of what the system had access to has an answer, which matters enormously for a claim about novelty and matters again for the provenance dispute this card returns to later.

That last point is worth stating as a general principle, because it applies well outside this. Freezing an external dependency turns an unbounded question into a bounded one. What did the system know is unanswerable against a live internet and answerable against a snapshot, and any system whose output will be scrutinised for originality wants that property before it produces anything rather than after. The pairing is also the standard shape for this kind of work, and recognising it is more useful than treating it as novel. A generator proposes, a cheap checker rejects most proposals, and only what survives is worth an expensive step. Code execution is the cheap checker here and Lean is the expensive one, and the whole run is a funnel with those two filters in it. Without a checker, scaling a generator up just produces more unverified output, which is not progress in any direction.

After the agents reached their result, a further 17 hours went into formalising and checking the proof in Lean. Lean is an interactive theorem prover with a small trusted kernel: you write a statement and a proof in its language, and the kernel mechanically verifies that the proof establishes the statement from the axioms. It does not read prose, it does not accept a gap, and it does not get tired at page 140 of 166.

That is a genuinely strong guarantee and it is precisely bounded, which is why it deserves stating carefully. What a Lean check establishes is that the formal statement follows from the axioms by the rules of the logic. Every step is present and every step is valid. For a long analytic argument, where the traditional failure mode is a lemma that is true in the cases the author considered and false in one they did not, this closes off the most likely way for a claimed proof to be wrong.

What it does not establish is that the formal statement is the theorem anyone cares about.

Between Fefferman's problem description and a Lean statement sits a translation, and the translation is done by humans and machines with no formal check of its own. Getting the function spaces right, the decay conditions right, the quantifiers in the right order, the notion of solution matching the one specified: each is an opportunity to formalise something adjacent to the intended claim and prove that instead. Nothing in the Lean toolchain can catch it, because the toolchain's job starts after the statement is written.

So the verification is real and the gap is in a specific place, and naming that place is more useful than either dismissing the check or over-reading it. The proof is machine-verified. Whether the machine verified the right proposition is a question for mathematicians reading the statement, which is exactly what the review period exists for, and it is why the Lean artefact accelerates the scrutiny rather than replacing it.

Terence Tao's objection is aimed somewhere else again and is worth carrying, because it is about value rather than validity. The primary worth of mathematical work, on his framing, is the digestible insight rather than the fact that a problem is closed; if the search process remains a black box, its value to mathematics is close to zero. A verified proof that nobody can extract a technique from settles one question and teaches nothing, and for a field whose output is understanding rather than answers, that is a real deficiency rather than a philosophical complaint.

Two mathematicians, Tristan Buckmaster at NYU and Levent Alpöge, had spent months working with AI systems on a closely related line of research on forced Euler equations. The overlap in subject and timing produced a question about where OpenAI's result came from, and the question has not been resolved. Buckmaster has said plainly that he has not seen the proof and does not know what the model did or how it worked.

OpenAI's position, as reported, is that the model did not have access to their specific work before publication, while acknowledging that it cannot rule out that de-identified data contributed to training. Those two statements are compatible and the second is the significant one, because it is an admission about a system property rather than about an incident: if product data flows into training in de-identified form, then the question of whether a particular user's work influenced a particular output is not answerable, by construction.

That is what makes this an engineering topic rather than a news item. Provenance of inputs is a property you build in or lack permanently, and it cannot be reconstructed after the fact. The cached corpus discussed earlier is the good version: a frozen snapshot means the question of what the system could read has an answer. The training data is the bad version, not because anything improper is established, but because the pipeline was not designed to answer questions of this shape and so cannot answer them now.

The priority dimension is separate and simpler. Two groups working the same problem is ordinary in mathematics and the discipline has machinery for it: preprints with dates, journal submission records, seminar talks. What is new is the possibility that one party's tooling saw the other's unpublished work, which the existing machinery has no answer for, because it was designed for a world where reading someone's drafts required them to hand them to you.

The transferable rule is short and unpopular. If a system's outputs will be scrutinised for originality, the provenance of its inputs has to be a designed property with an audit trail, decided before the system runs. Everything else, including a completely honest denial, reduces to a claim that cannot be checked, and a claim that cannot be checked is worth very little precisely when it matters most. The cached internet in this same system shows that OpenAI knows how to do this; the training pipeline shows what it costs when a component was not built for the question later asked of it.