Episode 24 — 10,000 Agents, 88 Hours: What OpenAI's Navier-Stokes Proof Reveals About Neuro-Symbolic AI

All opinions expressed are those of the individuals themselves, not necessarily of any company they work for.

This week's topic: OpenAI's Navier-Stokes result

Sunil Baliga: Token Drop, episode 24. Last week we talked about a timely topic, which was Astra, and following up on that, this week there's been a lot of discussion about this Navier-Stokes problem that's been solved by OpenAI.

Sunil: I remember vaguely learning about it in college — I think it was part of some computational fluid dynamics class, or something adjacent to that. I didn't actually take computational fluid dynamics, but something in that area touched on it. So it caught my attention, obviously, because I'd heard about it before, and there's been a lot of press.

Sunil: One of the things that stood out to me: it took 10,000 agents, according to the articles I read, working for 88 hours, to prove that the algorithm — or rather, that a smooth solution — didn't hold under all conditions. They token-maxed, for sure. I put myself in the shoes of the people working on this: you have 10,000 agents working for 88 hours. It looks like they're all throwing out ideas — how are they converging? How are they choosing? How does the system decide which is the right answer? After 88 hours, how do they know it's done? I don't know the answer to that. Maybe you two have more insight — Sajjad, Sam?

Sajjad's read: 10,000 agents, peer review, and a Lean-based verifier

Sajjad Khazipura: Thanks, Sunil. The Navier-Stokes equation is one I'd actually studied — it's one of the applications of partial differential equations. But I hadn't paid much attention to it, and I didn't understand the application context until, as you said, it suddenly burst into the open last week, with so much noise that it was genuinely hard to filter out what was actually going on.

Sajjad: If you focus on the science rather than the controversy: apparently, they used their latest internal model, built an agent around it, and created 10,000 instances of that agent. Those agents worked for roughly 88 hours continuously, throwing out candidate solutions. There was some informal peer review between those 10,000 agents to check whether a given answer was right or wrong. But the eventual adjudication was done by a completely separate pipeline, built on the Lean framework — which is nothing but a symbolic reasoner, in the same category Sam likes to talk about: Z3, Vampire, Datalog. So they depended on a Lean-based verifier to finally confirm which of those candidate solutions was actually correct.

Sajjad: That struck a real chord with me, because it's our approach too: no matter what model is generating the answer, you have to stand your ground and verify that answer using basic formalisms, and only then let the answer through. It harkens back to our own architecture — we have ClaimGuard as our verifier. We use less reasoning in it today than we'd like to, and Lean is exactly the kind of reasoning tool that was used here.

What is Lean? Symbolic verification, explained

Sunil: I'm not familiar with Lean. What is that — is it open source?

Sajjad: Lean is open source. It's a framework — almost like a language — for expressing logic rules, which you can then apply to symbolically verify whether something is right or wrong. Think about writing a basic C or Python application where you're comparing numbers — you write explicit logic: if A is less than B. Or take a sort algorithm: the heart of it is comparison. You take every pair of numbers, compare which is bigger and which is smaller, and swap them if you're doing bubble sort. You're doing a lot of symbolic processing — you understand the quantities, compare them, swap them, and run through the whole list.

Sunil's chip-design analogy: what do you verify against without a “golden” reference?

Sunil: This is really interesting. I always thought I understood ClaimGuard, and now, listening to this, I'm not sure I fully do — because it's making me think back to my chip days, where we talked about formal verification. You'd check the RTL against the implementation and see what went wrong. You had a master document to compare against.

Sunil: In this world — Navier-Stokes — how do you do a formal verification? How would we do it, or how does Lean do it? What are you comparing against — what's the golden list, so to speak?

How DaaX's own retrieval-and-verification pipeline actually works

Sajjad: In our case, the grounding documents are the source documents we're given. We extract content from those source documents and run it through our generation pipeline. We have a retrieval process — given a query, we go understand that query, and once we understand it, we search for the chunks of that document that match what we think are the potential answers.

Sajjad: It's a fairly convoluted process — you go through a graph, and the graph points to chunks of documents. Long story short: you find the right chunks that have the potential answer, and you give that question plus the potential answers to the LLM, which synthesizes a final answer.

Sajjad: Now, when the final answer comes out, we're not always sure which part of the document the LLM actually looked at to generate it. If there were two or three potential answers — say, “who was the President of the United States in 2020?” — and the LLM discovered there were multiple presidents at various points in time, it might say Obama was president in this timeframe, George Bush in this one, Trump in this one. Since LLMs can make mistakes even doing arithmetic, they're prone to making a mistake and giving you an incorrect answer.

Sunil's guess: verifying against the algorithm's own well-defined output

Sunil: How would it work in this case, then? Because with a document, you have a document — but here it's an algorithm. So maybe I'm guessing that the answer generated by one of these agents gets checked against the algorithm, and if it doesn't match, that's when the peer review kicks in to check and make sure. We're just speculating, of course — we don't actually know.

Sajjad: I think the problem had a well-defined input and a well-defined output — only the mechanism wasn't well known. It's like going from here to Boston. You can get there any number of ways, but what's the most efficient or correct way is left up to you. I think this problem fit that category — the verifier was used just to confirm whether a given pathway to the solution was correct. That's my understanding of how the solution was discovered.

Sam's numbers: 130 billion tokens, 2.7 million inter-agent messages

Sam Pooni: This is a very important thing from our perspective, since we're building neuro-symbolic systems. One of the main things to think about here is the sheer scale involved: about 10,000 concurrent agents, roughly 88 hours of research, 2.7 million inter-agent messages, and about 130 billion output tokens. And then another 17 hours, separately, for formalization and verification using the latest model.

Sam: So why does this matter so much? When we're building neuro-symbolic systems, we have a similar problem — especially translating natural language intent into SQL or any other DSL. There's a real probabilistic surface there: a deterministic side and a probabilistic side. The question is, can you eliminate the probabilistic surface entirely? That's an open research problem. But you can minimize it.

Why counterexamples, not just right/wrong labels, matter for neuro-symbolic systems

Sam: One of the things we think could get you there is a mechanism where you don't just say something is wrong — you also provide a counterexample. This is a very subtle but important distinction: what's the difference between proving something is right or wrong versus providing a counterexample?

Sam: This matters a lot in how the Navier-Stokes problem was structured. There were many isolated agent groups, each forming different formulations and different proof strategies, and the most important thing was the counterexample searches that came out of that. They combined all of this into intermediate results, and a consolidation layer — Codex — cross-pollinated those insights, so promising groups received combined insights from across the swarm. That's how the structure worked. From there, a candidate proof emerged, and it went through Lean for formalization and verification.

Sam: This is very significant, because it's similar to how our systems are, and will be, built in the future. They won't be built merely by saying “this is correct, this is wrong.” You need to provide a counterexample to train the LLM in a particular way — that's exactly why this is such an interesting problem for us.

The HPC era: brute force, the n-body problem, and drug discovery

Sajjad: What this harkens back to, Sam, is roughly the mid-1990s through 2010 — there was a lot of interest in HPC, high-performance computing, as a brute-force approach to similar problems. Think about the n-body problem: with two bodies, force is a function of their masses and inversely proportional to the square of the distance between them. But the moment you have three bodies, each exerting force on the other two, how does the whole system react? That was solved with brute horsepower — HPC.

Sajjad: Drug discovery was similar. You had all these different protein shapes, and the objective was to find a candidate molecule that would dock into a given protein shape. You could create that candidate molecule from any number of elements — combine a couple of carbon atoms with some hydrogen atoms, maybe an oxygen or nitrogen atom, and see whether it docks into the protein. If it doesn't, throw it away and create another candidate. You did this iteratively, through brute force, and it required large-scale HPC clusters.

What's different this time: intelligent candidate generation with a feedback loop

Sajjad: From what I've read, Navier-Stokes seems like a similar approach, but with one key difference: there's a feedback loop. The candidate generator is more intelligent — it's not just creating millions of random candidates, it's creating likely candidates, and it's taking feedback from the verifier. It has some intelligence, and it's using that intelligence to shorten and prune the candidate list, generating more realistic candidates for the verifier to check.

Could this have been done with old-school HPC? (88 hours vs. 88 days)

Sunil: So could this have been done in the old days with pure HPC? It would have just taken much longer — instead of 88 hours, maybe 88 days?

Sajjad: Quite likely it would have taken an intractable amount of time and an intractable number of compute resources. But given infinite resources, I'm reasonably certain it would have been an achievable solution. It's the old “give a million monkeys a million typewriters, and they'll randomly produce the works of Shakespeare” idea.

Sam: Here, though, with 10,000 LLM agents, this is really a parallel mathematics exploration problem. Where did we see something like this before? Neural architecture search — NAS — for finding new architectures. What I see here is agents conducting parallel mathematics exploration: generating candidate arguments, informally critiquing each other, and refining each other's intermediate results. That interplay between agents hasn't really happened before at this scale.

Sam: Separately, they built a Lean-based pipeline that formalized and machine-checked the resulting proof — that's a distinct piece. But the agent side — generating and evaluating ideas, proposing constructions, running computations, finding gaps, combining promising insights — that's one part of the story. The second part is that Codex cross-pollinated the groups: it consolidated useful intermediate findings, which needs to happen at every layer, because you need coordination to redistribute ideas across the group and bring everyone to the same understanding — much like people in a room arguing until they agree on the right approach, or agree that an approach is wrong.

Sam: One important clarification: Lean didn't discover the proof. Human validation remains necessary in this environment — it's not as though the machines solved this entirely on their own. The human in the loop is still there.

Not peer review — informal, adversarial swarm intelligence

Sajjad: I think there are two key things you just said, Sam. One: this was more akin to swarm intelligence compared to brute-force HPC methods, where you just throw thousands of GPUs or CPUs at the problem and keep creating random candidates, hoping one is the likely answer — finding a needle in a haystack, exhaustively, or Monte Carlo search if you're a bit smarter about it, but still brute force at the end of the day.

Sajjad: What this tells us is that it's almost a generational shift in solving intractable problems: a combination of brute-force methods with swarm intelligence, where agents talk to each other, learn from each other, criticize each other, shortlist better candidates, and a Lean verifier's feedback resets everyone's expectations on what's actually correct — gradually stepping toward the solution.

Sam: It wasn't peer review in the formal sense — in peer review, there's an independent review protocol. There was no independent review protocol here. It was informal, adversarial review: peer criticism and testing, not a formal peer-review process. That's what Sajjad's calling swarm intelligence — you counter an idea, that produces genuine back-and-forth, and that's what culminated in the shorter timeframe.

How the problem was actually routed: from Euler to Navier-Stokes

Sunil: Something else you said, Sam, and I have no real basis for this other than a gut feeling — 2.7 million messages seems too low to me. It feels like it should be a lot bigger. I have no basis to say that, but it just feels wrong.

Sajjad: If these agents are running continuously for 88 hours, and these are some of the most powerful models out there, I'd imagine they're communicating an enormous number of times.

Sam: You're looking at 130 billion output tokens — that's not a small amount. Actually, when I first read the story, it said 100 agents initially worked for roughly 50 hours and found a result — but that result was for a related Euler problem, not Navier-Stokes. OpenAI then identified this as a promising direction, moved agents away from less promising Millennium Problems, and gave the Euler result to the Navier-Stokes groups as new context, encouraging them to explore different approaches from there.

Sam: So it originally started on the Euler problem Sajjad mentioned, and Navier-Stokes is a different type of problem — but they moved away from the original target and encouraged exploration, then periodically used Codex to consolidate the best discoveries and inject those consolidated insights back into selected groups. That's the feedback loop.

Cross-pollination: explore, extract, redistribute, explore again

Sam: That cycle is called cross-pollination. This is very important for neuro-symbolic systems, and it's where we find this genuinely exciting: explore independently, extract useful insights, redistribute what you learned, explore again. That's the loop.

Sajjad: So what you're saying, Sam, is: given some really complex problem, you could have multiple instances of generative intelligence collaborate with each other, keep creating candidate answers, review among each other — and then eventually our ClaimGuard gets the opportunity to correct things, and the verification signal goes back to the generative subsystem, which learns from that feedback and improves. You're literally describing a closed feedback loop system.

The closed feedback loop, and why it maps directly to ClaimGuard

Sajjad: That loop can converge to better answers no matter how hard or intractable the problem is, because you're using a combination of intelligence and supercomputing horsepower to solve genuinely large, intractable problems.

Sam: Exactly — that's the beauty of it. Even in our own case, if we want to minimize the probabilistic boundary, you need to feed back: you found something wasn't correct, you gave a counterexample, and something has to take that information and improve on itself. What is that something? Until now, we didn't have the technology or the means to do that.

Sajjad: Today we have LLMs, so that can change.

Sam: Exactly — it never knew something, and now it's learning that. How do you do that? Through that loop.

Sajjad: This goes back to the story Sunil's talked about before — it's neither the LLM alone nor the symbolic system alone that works. Only when you put them together do they work well — almost like magic. That's exactly why we have the tagline “LLMs need a helping hand.” We have a verification system that helps the LLM do a better job.

Sam: When I looked at this, it was interesting from a pattern perspective — I was always thinking about the best approach to getting closer and closer to a target goal, and I could see that same pattern applied here in a different field: solving equations. But the underlying principle holds essentially the same.

Anima Anandkumar's physics-informed neural network: a different path, same result

Sajjad: Try solving the n-body problem through manual textbook, pen-and-paper methods — it's really hard. Two bodies attract each other with a describable force. Add a third body, and every body exerts that same force on the other two — they move by an infinitesimally small distance, which changes the force equations for all of them, because the distances have changed. That's the whole challenge, and we used to solve it with HPC. Now we're saying you can solve it with HPC plus some amount of intelligence thrown in.

Sajjad: Which brings up another interesting addition to this Euler/Navier-Stokes story: a separate effort by Anima Anandkumar. She's a researcher at NVIDIA and, I believe, teaches at Caltech. She built a physics-informed neural network paired with some kind of verifier operating in tandem — similar to OpenAI's approach — and it looks like they also reached convergence. There's a bit of controversy over who reached convergence faster on the exact same problem, but without getting into that controversy, it just tells us there were multiple intelligent pathways here: one was LLMs from OpenAI, the other was a physics-informed neural network trained extensively on physics equations, able to predict physics outcomes quickly.

Sajjad: I don't know which method was more efficient — less compute, less time — but the fact is there were multiple pathways to the same solution, largely using a combination of intelligence, HPC, and a verifier.

Wrap-up: neuro-symbolic systems need a formalized, machine-checked pipeline

Sunil: I think we've run out of time. Anything else, Sam?

Sam: I think the overall point we've been making is clear: neuro-symbolic systems require, more or less, a formalized pipeline with machine-checked verification, and the resulting proof runs through a separate pipeline. That's the whole idea. I think we're getting there, and our notion of grounded truth is on the same plane. This is very relevant to people developing agents — they can understand how these agents interact, how informal adversarial review works, and take this as a pattern worth studying. There are deeper problems we could solve using this same approach, both in grounding and in predicting intent more carefully. I think this is a fascinating area, and a great methodology to look at for building future systems.

Sunil: Okay, we're out of time. Thank you both — we'll talk to you later.

Sajjad: Thank you.