Navier-Stokes and augmented intellectual work

Artificial Intelligence

EU AI Act consulting: system classification, policies, AI governance, training.

Discover →

Linux Services & Systems

Domains, hosting, PEC, email infrastructure, network services and Linux systems. Open Source infrastructure support and management.

Discover →

Yesterday Stefano Noferi wrote about the Navier-Stokes proof: what the statement says, which of Fefferman’s four formulations was resolved, why the version with an external force does not weaken the result, and how the credit dispute with Tristan Buckmaster and Levent Alpöge opened up. That part is mathematics.

Here we look at the other half of the same document, which is an operational account of how the result was produced. It is the part that concerns anyone working with agents, because it describes a mode of intellectual work that will not stay confined to mathematics.

The declared figures

All of them come from the OpenAI document, with no supporting sources.

• The model used is internal, in training since 28 August, with training still ongoing. OpenAI describes it as “significantly more capable than GPT-6 Astra”.
• The effort starts on Tuesday 1 September, after rumours reach the company that two Millennium Prize problems had been resolved. The decision is to evaluate the model on all open problems, plus a set of other high-impact ones.
• The agents have two tools: reading from a cached copy of the internet and running code. They are split into groups, with communication inside each group.
• The group that closes Navier-Stokes is on the order of 10,000 concurrent agents.
• The solution arrives on Saturday 5 September, roughly 88 hours after launch.
• Lean formalisation and verification cost a further 17 hours, via GPT-6 Astra.
• Navier-Stokes alone consumes 2.7 million messages and about 130 billion output tokens. Across all attempted problems the totals reach 4.9 million messages and about 300 billion tokens.

Where the decisions were taken

The document is unusually explicit about what the people did, and that list is more interesting than the token count.

Choosing the form of the statement. The variants were assigned to separate groups: A and B to those who had to prove regularity, C and D to those who had to disprove it. This is not an organisational detail. The two directions ask for opposite things, and launching them in parallel is how you proceed when you do not know which one is true.

Putting the side problems on the list too. Alongside the large problems, a set of questions declared easier was included. That is where the unforced Euler result came from, obtained by roughly 100 agents in 50 hours.

Recognising that the side result was the lever. Once the Euler solution appeared, resources were shifted onto Navier-Stokes and the Euler resolution was handed to the agents as starting material. When a further trained version of the internal model became available, the agents were updated mid-run.

Circulating insights between groups that were not talking to each other. The groups communicated only internally. At a certain point Codex was used to consolidate the most useful insights from each group and to build the follow-up prompts from the agents’ own intermediate results. The group that closed Navier-Stokes was guided this way.

Deciding to formalise. It was not compulsory, and it is the choice that changes the nature of what was published.

None of those five is a model capability. They are framing and allocation decisions: which problem, in which form, with how many resources, when to move them and when to stop. That is the part of intellectual work that stays with whoever is leading, and it is the same part that stays with a researcher who works with an instrument instead of ten graduate students.

Lean is the piece that makes the rest usable

Eighty-eight hours of exploration produce a volume of material nobody will read: 2.7 million messages cannot be reviewed. Seventeen further hours produce an object of a different nature, a proof formalised in Lean, which a proof assistant checks mechanically.

The property that matters is this: verification does not depend on trusting whoever produced the proof. There is no need to know whether ten thousand agents, a doctoral student or a research group stood behind it, and no need to reconstruct the path. The check is on the artefact.

It is the same pattern we have followed in very different cases. With zero-knowledge proofs on inference the proof makes a computation verifiable without having to trust whoever ran it. In the Model Hardware Standard the agent stops short of the instrument and produces an inspectable script that a human reads and signs. Here Lean plays that role, and plays it better, because the verifier is deterministic.

The flip side is that this pattern does not travel everywhere. It holds where a mechanical oracle exists.

The ratio between produced and usable

The most instructive figure in the document is not the number of agents but the ratio. Out of 2.7 million messages and 130 billion output tokens, what remains is one writeup and one formalisation. Everything else is discard, and the discard is the condition of the result rather than a defect of the method.

Anyone planning to put agents on hard problems would do well to read that ratio as a cost line. Generation is the cheap part. The filter is the expensive part, and if the filter is human it does not scale alongside generation. We had already measured this on far more prosaic ground: in the study on model-generated patches, 26% of the fixes closed the flaw without the code changing in any sensible way. Without something that verifies, the quantity produced does not become available quality.

One point on the operational context, since it is what we have been writing about for days: a group of ten thousand agents communicating with each other and exchanging intermediate results is the same organisational shape we described when writing about coordination nobody asked for. Here the coordination is designed, isolated and monitored, and OpenAI states it applied the same safeguards used in its other frontier model evaluations. The difference between the two cases is not agent capability. It is that somebody decided the topology in advance.

Why science is not all mathematics

The limits of the transfer need saying plainly, otherwise the reading turns promotional.

Mathematics has a mechanical oracle. The Lean kernel says yes or no, and the cost of that answer is independent of how hard the discovery was. In fields with an equivalent checker the conversion is direct: formal proofs, code with tests and types, formal verification on circuits, simulations constrained by conservation laws. There, vastly wider exploration genuinely becomes a result third parties can use.

In fields where verification is empirical the bottleneck moves into the laboratory. One hundred and thirty billion tokens do not shorten a clinical cohort, do not replicate an experiment and do not produce a sample. What changes is the work that comes before: literature reviews, hypothesis formulation, study design, analysis. That is augmented intellectual work, and there will be more and more of it, but the augmented part sits upstream of the evidence.

The second limit is availability. The model that produced the proof is internal and unreleased, declared more capable than GPT-6 Astra. What is reproducible today is the method, not the capability. And declared capability has to be kept distinct from verifiable capability, which is exactly the theme we worked through reading the GPT-6 Astra tables, where how the test was built changed the number.

What we think

There are three pieces in this story and they only work together: parallel exploration with a very high discard rate, a deterministic check that does not depend on the author, and a person who decides where to aim and when to stop. The piece almost always missing, in the projects we see, is the second one.

For anyone in research and development weighing up putting agents on serious problems, the practical consequence is ordinary and not very exciting: build the verifier first, then widen the exploration. Tests, types, invariants, reproducible builds, inspectable scripts, benches with a success criterion written beforehand. They are the everyday version of what Lean was here. Without them you produce ten thousand results and cannot use any of them.

There is finally a consequence for the credit dispute, which Noferi reconstructs and which we are staying out of. A formalised result narrows the field of what remains contestable: priority carries on being a matter for argument, as has happened many times in the history of mathematics, while whether the proof holds is settled by the verifier. For a science done with instruments that produce far more than a reviewer can read, that narrowing is the thing worth taking away.

Sources

• OpenAI, On the Navier–Stokes Millennium Prize Problem
• Clay Mathematics Institute, official problem formulation (PDF)
• Stefano Noferi, the proof and the four formulations
• GPT-6 Astra: has the AGI era really begun?
• Zero-knowledge proofs on inference
• Model-generated patches: 26% close the flaw without changing the code