OpenAI's Navier-Stokes blow-up claim: A claimed blowup for the fluid equations
OpenAI
OpenAI says some 10,000 agents running an unreleased model proved forced Navier-Stokes blowup, checked in Lean. Clay calls the problem apparently settled yet lists it as open; experts dispute the Lean match and the credit.
What OpenAI announced on 8 September
On Tuesday 8 September 2026, OpenAI published a post titled On the Navier-Stokes Millennium Prize Problem stating that an internal system had produced a proof that the three-dimensional incompressible Navier-Stokes equations, which govern viscous fluids such as water and air, can develop a singularity in finite time. Two artifacts came with it: a 166-page manuscript, Finite time blowup for Navier-Stokes, credited simply to "OpenAI" with no individual authors, and a public repository of Lean 4 formalizations. The post says the work resolves the Millennium Prize problem by establishing statement C, and also statement D, of the official formulation. In the same document the company says it does not intend to claim the prize.
The theorem itself is narrower than the headlines that followed. Theorem 1.1 of the manuscript asserts that, for every positive viscosity, there is a force that is smooth and confined to a bounded region of space and a bounded window of time, together with a smooth velocity and pressure defined up to time 1, such that the fluid starts at rest, stays inside a fixed compact region, keeps bounded kinetic energy, and yet has a maximum speed that grows without bound as time approaches 1. The conclusion drawn is that no smooth, finite-energy solution with that force and that starting state can exist for all time. Because the force and the flow are compactly supported, the same construction can be placed inside a periodic box, which gives the torus version.
OpenAI also posted a second, 57-page manuscript, Finite time blowup for the Euler equation, claiming blowup for the inviscid Euler equations with no external force at all, starting from smooth, compactly supported initial velocity. That claim needs no force, but the Euler equations are not a Millennium problem and the paper has drawn less scrutiny.
What the Clay problem actually asks
The Clay Mathematics Institute's official problem description, written by Charles Fefferman, writes the equations for an incompressible fluid filling all of three-dimensional space, including an external force term, and then restricts attention to physically reasonable data. Initial velocities and forces must be smooth and must decay faster than any power of distance (for the force, also of time), and acceptable solutions must stay smooth for all time and, on the whole space, keep bounded energy. Fefferman then offers four statements and asks for a proof of any one of them. Statements A and B assert that, with the force set identically to zero, smooth solutions exist forever for every smooth initial velocity, on the whole space and on the periodic torus respectively. Statements C and D assert breakdown: that some smooth initial velocity and some smooth force satisfying the decay conditions admit no such global smooth solution.
So the letter of the official statement allows a force. A blowup driven by a smooth, rapidly decaying force is what alternative C describes, and a force supported in a compact region of space and time satisfies the decay conditions automatically. That is why OpenAI's repository maps its two theorems onto C and D, and why Scientific American's October analysis describes forcing as a loophole in Clay's official framing rather than a departure from it. It is therefore inaccurate to say that a forced result answers a different problem from the one Clay posed. What it does not answer is the question most people picture: whether a fluid left alone, with no force, can develop a singularity. Statements A and C are not contradictory. A proof of C leaves A, the unforced global regularity question, exactly as open as it was.
Clay's own position as of 27 October 2026 is measured. In a statement dated 11 September, the Institute said it shared the community's excitement at the announcement that the problem "has apparently been settled," and that its evaluation process is "deliberately unhurried." Its Navier-Stokes problem page still carries the label Active. Under the Millennium Prize rules adopted in 2018, Clay will not consider a proposed solution until it has appeared in a qualifying outlet, at least 2 years have passed since that publication, and it has received general acceptance in the global mathematics community. None of the sources reviewed here reports a refereed publication by late October, so under those rules the earliest any consideration could begin is late 2028.
The road to a forced singularity
Whether three-dimensional viscous flow can break down has been open since Jean Leray's 1934 work on weak solutions, as the OpenAI manuscript's own historical section recounts. Two lines of work shaped the decade before this claim. One was structural. Terence Tao's construction of blowup for an averaged Navier-Stokes equation showed that any proof of global regularity would have to exploit finer structure in the nonlinear term than the energy identity and standard estimates provide. The other was computational. Numerical work by Thomas Hou and collaborators suggested an Euler singularity in a spinning cylinder, and Jiajie Chen and Hou later turned it into a computer-assisted proof of blowup from smooth data in a domain with a boundary. In January 2026 a team including Tristan Buckmaster and Google DeepMind researchers used physics-informed neural networks to report new candidate unstable singularities in the Euler equations and simpler model equations, none of them yet proved.
The line OpenAI's work was first said to follow came from Madrid. Diego Córdoba and Luis Martínez-Zoroa showed in 2023 that the forced three-dimensional Euler equations can blow up, with a force that stays bounded in a Hölder class just above one derivative but is not smooth. The OpenAI manuscript describes their mechanism as successive amplification of ever more concentrated vortex layers, larger-scale strain feeding smaller-scale vorticity. The open step was to make the force fully smooth. In September 2026, Levent Alpöge, a mathematician employed by Anthropic, and Buckmaster, at New York University, released heavily AI-assisted results doing that for several equations, including, with Matei Coiculescu, blowup for the incompressible porous media equation with space-time smooth forcing. Tao's blog post of 7 September described their porous media, Boussinesq and Euler results with smooth forcing, noted that they had been formalized in Lean, and judged the Navier-Stokes analogue very feasible but not yet achieved.
How the construction is supposed to work
The manuscript's physical description begins with an observation that explains both the power and the weakness of forced constructions. For any incompressible flow, one can define the force as whatever is left over when that flow is substituted into the equations, so the equations hold by construction. The whole difficulty is to choose a flow that blows up while the leftover stays smooth, including at the instant of blowup, where individual terms diverge and must cancel one another.
The chosen flow is a vortex: a column of fluid spinning about a vertical axis, spiralling inward and streaming out along the axis in both directions from a central layer. Write tau for the time remaining before the singularity. The core's radius shrinks like the square root of tau while its height shrinks slightly more slowly, so the column grows ever more slender. Its spin and axial speeds grow faster than one over the square root of tau, while the radial Reynolds number stays bounded, so viscosity keeps competing with the inflow instead of being swamped. Because the core's volume shrinks faster than its speeds grow, its kinetic energy actually tends to zero. Joining this core to a slower outer flow leaves a residual that would itself blow up, so the construction adds rings of rapidly oscillating pulses whose averaged momentum flux cancels the singular part of that residual, followed by corrections to every order. What remains is a force that extends smoothly through the singular time, acting on a fluid that started at rest.
OpenAI's post states the goal in plain terms: the breakdown must come from the motion of the fluid itself, not from an infinite force inserted by hand. How much work the smooth force is doing became one of the first questions specialists tested. Peter Constantin, Mihaela Ignatova and Vlad Vicol proved that, for solutions sharing two structural features of OpenAI's construction and with a force bounded in two derivatives, the force can neither vanish near the singular point nor be real analytic in space. In this family of constructions, in other words, the force cannot be removed. Separately, Shaozhen Cao, Zhuoni Chi and Ping Nie took OpenAI's compact blowup as given and showed that forces producing blowup are dense in a weak topology: arbitrarily close to any smooth solution, in that sense, sits a smooth force that drives a singularity. Both papers use the construction as a starting point, and both sharpen how far a forced singularity lies from an unforced one.
Ten thousand agents and a Lean certificate
The discovery process is documented only by OpenAI. According to its post, the company had been training a new internal model since 28 August, built by large-scale reinforcement learning on a pretrained base and described as significantly more capable than GPT-6 Astra. On 1 September it heard rumors that two Millennium problems had been resolved and set coordinating agents on every open Millennium problem and some easier targets. Agents could read a cached copy of the internet and run code. Separate groups were prompted with statements A and B, which would require proving regularity, and with C and D, which would require constructing a breakdown. Nearly 100 agents produced the unforced Euler result in about 50 hours, after which OpenAI moved agents to Navier-Stokes with the Euler proof in hand, used its Codex product to consolidate insights across groups, and switched the agents to a further-trained model midway. The successful group involved on the order of 10,000 concurrent agents and reached its result on Saturday 5 September, about 88 hours after the first launch. Formalization in Lean took another 17 hours using GPT-6 Astra. For Navier-Stokes alone, OpenAI reports 2.7 million messages and about 130 billion output tokens.
OpenAI's Sébastien Bubeck told Quanta Magazine that the effort cost several million dollars. Noam Brown of OpenAI, as reported by The Decoder, credited less than 10 percent of the success to the multi-agent setup and the rest to the underlying model, while The Decoder noted that nobody knows what the swarm contributed and that no one has tested a single agent on the same problem.
The target statements in the repository are not OpenAI's own wording: the repository's Comparator instructions credit an adapted formalization of the Navier-Stokes problem statement from Google DeepMind's Formal Conjectures project. In a guest post on Tao's blog dated 9 October, the mathematician Thomas Hales reported that the Navier-Stokes formalization had been confirmed by more than a dozen proof checkers. He stressed that a human must still audit the formal statement, down to how it defines real numbers, derivatives and measure, to confirm that it says what Fefferman's statement says, and he noted that such an audit is far easier than checking a proof.
Where verification stands
A compiled Lean proof of a faithful statement would settle the theorem, but it does not certify the 166-page prose argument that mathematicians would read, cite and build on. That gap is the subject of a paper posted on 6 October by Alexander Bastounis, Fabian Circelli and Anders Hansen, who show that the Lean proof does not correspond to the natural-language proof. In one example, Lemma 8.6 of the manuscript bounds an inverse operator using four extra derivatives of its input, while the Lean lemma cited for it needs five. In another, the Lean proof of a pressure-flux estimate takes a different route through different inequalities and reaches a different bound. Their conclusion is that the manuscript asserts stronger intermediate statements than the formal proof establishes, so the Lean check offers no assurance that the prose is right. They are explicit about the limits of their own claim: they make no judgment on whether OpenAI's prose proof is correct, and they accept that the Lean code shows the formal theorem holds. After preliminary checks, they also predict a high likelihood of substantial mistranslation in the Euler formalization. The preprint also argues more broadly that resolving the ambiguities of mathematical prose, which faithful translation requires, is harder in the Solvability Complexity Index hierarchy than even the halting problem, so no AI autoformaliser can guarantee a faithful translation. A King's College London press release publicized the paper on 27 October, noting that the authors have not shown OpenAI's proof or its result to be wrong; it adds no new check of the mathematics.
Scientific American reported on 13 October that top experts find the paper hard to read and that several research groups are using the Lean code and the manuscript, with help from other language models, to produce simplified accounts. The article's author, Joseph Howlett, wrote in his own voice that OpenAI did not understand its own model's proof and that a month on no one fully did. The Decoder relayed that account on 17 October and added that roughly 400 further results OpenAI posted to GitHub in early October had angered mathematicians who felt the volume cheapened their field. Quanta's original headline had declared the problem solved, while its text conditioned that on the result holding up to further scrutiny.
In short, as of 27 October 2026 the formal theorem is machine-checked but its statement audit is not reported as published, the prose proof is unrefereed and not mirrored by the formal one, no specialist group has reported verifying the prose end to end, OpenAI's Lean repository shows no change since 10 September, and Clay has said nothing since its September statement.
The dispute over credit and method
The announcement landed inside a priority dispute. Just before midnight on Monday 7 September, Buckmaster posted a statement announcing his and Alpöge's results. Quanta reports that they had a Lean-verified forced Euler proof by 22 August and brought their release forward after word of their progress reached OpenAI, whose announcement followed about 12 hours later. Scientific American's first report carried Buckmaster's allegation that OpenAI had learned of their progress in the preceding week and adopted their method, and Bubeck's denial at a press briefing that OpenAI had used their prompts or proofs to prompt its models.
OpenAI's post gives its own timeline. It began on 1 September after a rumor it later connected to Alpöge and Buckmaster, contacted them after finishing its Lean verification on 6 September to offer a joint announcement, recognized their priority on the forced Euler problem, and says an internal investigation confirmed that Buckmaster's prompts to its Codex product over the preceding two months could not have influenced the system. Scientific American later reported a further allegation by Buckmaster that OpenAI had tried to bribe and threaten him to keep him from going public; the only OpenAI response the article recorded concerned whether its model could have seen his data. Camillo De Lellis of the Institute for Advanced Study told the magazine he saw no factual resolution of the question, which The Decoder linked to the black-box nature of the models. Bubeck had already answered the threat allegation in public. Buckmaster's public statement says that on 6 September Bubeck twice said he wanted Alpöge removed from authorship and asked why Buckmaster would ruin his career by going public. On X on 8 September, as The Next Web reported, Bubeck denied seeking Alpöge's removal from his own work and apologized for the career remark as an extremely poor choice of words, and Sam Altman defended the team. The outlet could not verify either side's account of the private calls.
On method, the account has shifted. OpenAI officials initially described the proof as following the Córdoba and Martínez-Zoroa program, and Fefferman, the author of the official problem statement, told Quanta that he was thrilled the problem was solved and that the two Spanish mathematicians were the heroes of the story. By October, according to Scientific American, experts working through the paper agreed that the resemblance was superficial. Gonzalo Cao-Labora of EPFL put it this way: "When you go to the details, it is a different approach." The magazine reported that a smaller early group of agents may have followed the Spanish program for an intermediate result, while the large swarm found a different path. If that reading holds, the quarrel concerns inspiration and timing more than shared mathematics, a judgment others may contest. On 11 September a declaration, A Severe Misalignment of AI in Mathematics, now signed by 28 Fields medalists, argued that AI results announced in a rush leave no time for proper write-ups or citation of earlier work and raise severe attribution questions. It names no company and judges no particular proof.
The honest limits
Several things are not claimed, or not established. The unforced problem, statements A and B, is untouched: a proof of C is logically compatible with every smooth unforced flow staying smooth forever. The direct physical stakes are small. The singularity requires a force tuned to cancel the flow's own divergences, and Quanta notes that real fluids are made of molecules, so infinite speeds in the idealized equations would not occur in nature. The result of Constantin, Ignatova and Vicol indicates that this route cannot simply be continued to a force that switches off near the singularity, which is what an unforced blowup would need.
On the machine side, the model is unreleased, the agent transcripts are not public, and no outside party can rerun the search, so every process figure (agent counts, hours, tokens, the role of the Euler result, the sequence of events from 1 to 6 September) rests on OpenAI's own account. How credit divides among the base model, the swarm, and the human researchers who chose prompts and consolidated intermediate results is undocumented. The unforced Euler claim, potentially the more surprising mathematics, has had even less independent examination, and the only public assessment of its formalization so far is the prediction of mistranslation noted above. Finally, the prize is not in play in the near term: OpenAI says it will not claim it, and Clay's rules would defer any consideration for years regardless.
How to place the claim in AI history
If the theorem stands, this is the first time an AI system has produced a proof of one of the four statements Clay offers for a Millennium problem, delivered with a machine-checked formal certificate, within weeks of the model's own training run beginning. It extends a fast sequence: olympiad gold in natural language in July 2025, then an OpenAI model's disproof of Erdős's unit distance conjecture in May 2026, and now a claim at Millennium scale, with effort measured in billions of tokens and thousands of concurrent agents rather than in a single model's answer. It also inherits the reinforcement-learned reasoning approach that OpenAI introduced with o1.
What the episode most clearly shows, as of 27 October 2026, is a shift in where the bottleneck sits. Producing a long, formally checked argument is no longer the scarce step. Reading it, auditing the formal statement, confirming that the prose matches the code, and assigning credit are. Hales's call for statement audits, the mismatch documented by Bastounis, Circelli and Hansen, and De Lellis's doubt that the priority question can be settled at all are three versions of that same problem. The forced question may well now have an answer that specialists are prepared to build on. Whether it deepens human understanding of fluids, which is what Clay's statement says it hopes for, depends on the slow human reading now under way, and any judgment of lasting influence has to remain provisional until that reading is done.
References
- OpenAI (2026). On the Navier-Stokes Millennium Prize Problem.
- OpenAI (2026). Finite time blowup for Navier-Stokes.
- OpenAI (2026). Finite time blowup for the Euler equation.
- OpenAI (2026). NavierStokesAndEuler: Lean certificates accompanying the Navier-Stokes and Euler results.
- OpenAI (2026). Comparator challenges for the Navier-Stokes and Euler formalizations.
- Fefferman (2000). Existence and Smoothness of the Navier-Stokes Equation.
- Clay Mathematics Institute (2026). Navier-Stokes Announcement.
- Clay Mathematics Institute (2026). Navier-Stokes Equation: Millennium Prize Problem page.
- Clay Mathematics Institute (2018). Rules for the Millennium Prize Problems.
- Quanta Magazine (2026). AI Has Solved One of Math's $1 Million Millennium Prize Problems.
- Scientific American (2026). OpenAI claims blockbuster math breakthrough amid swirl of controversy.
- Scientific American (2026). OpenAI's blockbuster Navier-Stokes proof isn't what we thought it was.
- The Decoder (2026). Mathematicians say OpenAI doesn't understand its own Navier-Stokes proof.
- Bastounis, Circelli and Hansen (2026). Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs.
- Hales (2026). What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI.
- Tao (2026). Finite time blowup with smooth forcing term for the incompressible porous medium, Boussinesq, and incompressible Euler equations.
- Córdoba and Martínez-Zoroa (2023). Blow-up for the incompressible 3D-Euler equations with uniform C1,1/2-ε and L2 force.
- Alpöge, Buckmaster and Coiculescu (2026). Extending the Córdoba-Martínez-Zoroa IPM Blow-Up to Uniformly Space-Time Smooth Forcing.
- Constantin, Ignatova and Vicol (2026). Regularity of asymptotically axisymmetric solutions to the 3D Navier-Stokes equations with analytic forcing.
- Cao, Chi and Nie (2026). Density of Forces Producing Navier-Stokes Blowup.
- Tao (2014). Finite time blowup for an averaged three-dimensional Navier-Stokes equation.
- Buckmaster (2026). Statement announcing the smooth-forcing blowup results.
- Constantin, The Next Web (2026). OpenAI's Bubeck denies trying to cut Anthropic mathematician from credit.
- Math and AI (2026). A Severe Misalignment of AI in Mathematics.
- King's College London (2026). OpenAI's Navier-Stokes proof called into question.
- Chen and Hou (2022). Stable nearly self-similar blowup of the 2D Boussinesq and 3D Euler equations with smooth data I: Analysis.
- Quanta Magazine (2026). Using AI, Mathematicians Find Hidden Glitches in Fluid Equations.
Cite this report
Chronicle. (2026, October 27). OpenAI's Navier-Stokes blow-up claim (2026): A claimed blowup for the fluid equations. https://epoch.founden.co/events/navier-stokes-claim
Connected developments
Follow the ideas behind this event and the developments that came after it. Connections indicate conceptual or historical relationships, not proof of sole causation.
Reinforcement-learned reasoning · 2024OpenAI o1: Thinking before answeringOlympiad proofs a year earlier · 2025AI gold at IMO 2025: Olympiad gold in natural languageEarlier OpenAI research result · 2026Erdős unit distance disproof: Erdős's grid is finally beatenModel that formalized the proof · 2026GPT-6 Astra · Astra: the next frontierSame model's 722-paper release · 2026OpenAI's quasi-Riemann hypothesis proof: A claimed fence around zeta's zerosLater Lean-checked claim · 2026Exponential Time Hypothesis refutation: Two labs claim 3-SAT escapes exponential time