# OpenAI's Navier-Stokes claim ships with a Lean proof. The fight is over everything else URL: https://www.thedeepfeed.ai/posts/2026-09-09-openai-navier-stokes-claim/ Category: Research Published: 2026-09-09 Author: the-deep-feed Tags: mathematics, openai, lean, navier-stokes, formal-verification Kind: news > OpenAI says an internal model proved the forced version of Clay's Navier-Stokes problem and released a Lean certificate anyone can check, but the first day of reaction turned on what no certificate settles: whether forcing answers the real question, and who got there first. ## TL;DR - **OpenAI** claims an internal model proved that a smooth fluid at rest, pushed by a **smooth external force**, can blow up in finite time, which is statement C (and D) in the official Clay formulation, after about **10,000** concurrent agents worked for **88 hours**. - The release includes a **166-page** paper and a GitHub repository of **2,486** Lean files checked against a 286-line statement adapted from Google DeepMind's Formal Conjectures, written in May, months before OpenAI's run. - The first-day fights were about what Lean cannot check: whether forced blowup is the question mathematicians meant, and credit, after **Tristan Buckmaster** said OpenAI turned to the problem only once word of his work with Anthropic's **Levent Alpöge** spread. On September 8, OpenAI [announced](https://openai.com/index/navier-stokes-solution/) that an unreleased internal model had resolved the Navier-Stokes existence and smoothness problem, one of the seven Millennium Prize Problems the Clay Mathematics Institute named in 2000. The company published a [166-page paper](https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf) and a [Lean formalization](https://github.com/openai/NavierStokesAndEuler) that a computer can check line by line. That pairing makes it one of the most checkable claims on a famous open problem ever put before the field. It also means the arguments that broke out within hours were about the two things a proof checker cannot reach: what question was answered, and who started answering it first. # What OpenAI claimed, exactly The claim is narrower than the headlines. OpenAI says its system proved "that an initially smooth fluid at rest can develop a singularity in a finite time," and that "the fluid has a smooth force applied to it." That, the post says, "resolves the Navier–Stokes Millennium Prize problem by establishing statement 'C' (and also 'D')" of the [official problem description](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf) written for Clay by Charles Fefferman. Statement C is breakdown on ordinary three-dimensional space; D is the same on a periodic box. OpenAI says it began training the internal model on August 28, heard "rumors that two Millennium Prize problems had been resolved" on September 1, and pointed agents at every open Millennium problem. A warm-up target, finite-time blowup for the unforced Euler equations (Navier-Stokes without viscosity), fell first, to "nearly 100 agents" working for "approximately 50 hours." The company then moved its agents to Navier-Stokes, where the group that found the proof ran on the order of 10,000 concurrent agents and finished on Saturday, September 5, about 88 hours after launch. GPT-6 Astra spent 17 more hours on the Lean formalization. Across all problems the agents sent 4.9 million messages and used about 300 billion output tokens; Navier-Stokes alone took 2.7 million messages and roughly 130 billion tokens. Mark Chen, OpenAI's chief research officer, told [AFP](https://www.ctvnews.ca/sci-tech/article/openai-says-ai-solved-one-of-maths-hardest-problems-in-days/) the compute ran "emphatically in the millions of dollars." The post adds: "We do not intend to claim the Millennium Prize for this result." # What was released, and what it can check The [NavierStokesAndEuler repository](https://github.com/openai/NavierStokesAndEuler) was created on the morning of September 8 with a single commit holding 2,486 Lean files, about 32 megabytes of source, 643 of them for Navier-Stokes and 1,839 for Euler. Nobody will read that by hand, and nobody has to. The README points to Comparator challenges, the Lean community's tool for confirming that a proof proves an agreed statement from permitted axioms, and its instructions call for nanoda, an independent proof checker, alongside Lean's own kernel. The statement being checked is the strongest part of the package. The [challenge file](https://github.com/openai/NavierStokesAndEuler/blob/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538/ComparatorChallenges/NavierStokes.lean) says it is "copied from" Google DeepMind's Formal Conjectures project at a pinned commit, with the upstream definitions and both breakdown alternatives "retained." That upstream file [was first added](https://github.com/google-deepmind/formal-conjectures/commit/641ff32207fdcf4fdf6aeda4dbb02f6d9be0c251) on May 15, 2026, more than three months before OpenAI started training the model. OpenAI's adaptation runs to 286 lines, which a specialist can audit in a sitting. If the kernel is sound and those 286 lines say what Clay says, the 32 megabytes are correct whether or not anyone understands them. For a claimed proof of a famous problem, where checking usually means years of referees reading prose, that is new. It narrows the dispute without ending it, because the certificate inherits whatever latitude the statement allows. # The forcing question Fefferman's statement C asks for "a smooth, divergence-free vector field u°(x) on R3 and a smooth f(x, t)" for which no smooth solution exists. The *f* is an external force, and it is in the official text. According to *Scientific American*, most experts write the problem without that term, assuming any blowup should look the same with or without it. The [magazine](https://www.scientificamerican.com/article/ai-may-have-just-solved-a-million-dollar-math-problem-the-field-will-never-be-the-same/) named the difficulty on announcement day: "The Clay problem, as written, is solved. But the Clay problem, as many experts imagine it, lacks the piece that the forcing method relies on." It added that it is unclear whether the proof can be extended to the unforced equations at all, leaving "the Clay Institute, and the field of mathematics, in a bit of a quandary." The forced route was not new on September 8. Diego Córdoba and Luis Martínez-Zoroa developed it over several years, and hours before OpenAI's post, NYU's Tristan Buckmaster and Anthropic's Levent Alpöge used it to release smooth-forcing blowup results for the porous media, Boussinesq and 3D Euler equations. Terence Tao wrote about their papers within hours of their release, and his assessment reads differently now: > There does not seem to be anything in principle preventing the methods from extending all the way to Navier-Stokes, and there is even a non-negligible chance that the forcing term could be eliminated entirely, although there are an enormous number of technical difficulties that would ensue in implementing that program. At this point, I would not be surprised if one could batter out such an extension by pouring an enormous amount of compute and AI assistance at such a task. > > — [Terence Tao, Mathstodon](https://mathstodon.xyz/@tao/117233528517340774), Sep 8, 2026 # Who got there first The credit dispute arrived before the claim. Buckmaster's [four-page statement](https://cims.nyu.edu/~tristanb/statement.pdf), posted with the papers, says he and Alpöge had smooth-forcing blowup for Boussinesq and Euler on August 15, verified the first proof in Lean on August 22, and chose not to rush a certificate out ahead of a readable paper. He writes that he emailed an OpenAI mathematician on September 3 about rumors attached to his name, then spoke with that mathematician and OpenAI's Sébastien Bubeck twice on September 6. In his account, OpenAI proposed that he alone write up its Navier-Stokes proof, Bubeck "twice asserted that he wanted Levent removed from authorship," and when Buckmaster said he would go public he was asked, "Why would you ruin your career?" Asked whether OpenAI's model had been trained on his group's Codex sessions, he "did not get an answer." OpenAI's post acknowledges that its effort began after "a rumor which we later realized was related to" Alpöge and Buckmaster, and says neither its researchers nor its agents saw their work before release. Bubeck [wrote on X](https://x.com/SebastienBubeck/status/2097379411691516310) that he "never ever asked for Levent to be removed from authorship of his own work" and apologized for an "extremely poor choice of words." Sam Altman [defended the team](https://x.com/sama/status/2097385167002415140) while confirming the rumor was the trigger. The company's follow-up kept one door open: > We (the researchers and the agents) did not see any of their work through any means until they released it publicly — in particular, no specific user data was accessed in order to solve this problem. > > While unlikely, we cannot rule out that de-identified data derived from their usage of our products helped improve our models. > > — [@OpenAI](https://x.com/OpenAI/status/2097375276384567642), Sep 8, 2026 That sentence drew the sharpest follow-up. On September 9, the mathematician Andreas Thom [recalled](https://mathstodon.xyz/@andreasthom/117240535270608201) asking OpenAI, after an earlier result built on his methods, whether his ChatGPT conversations had entered training data or been accessible during solving, and receiving only: "Regarding your conversations with ChatGPT: that did not happen." Whether researchers can trust OpenAI with unpublished mathematics, he wrote, is a "serious, unanswered question." The [Hacker News thread](https://news.ycombinator.com/item?id=49613262) passed 1,100 points by early September 9, with the data sentence quoted throughout. # What Clay will do, and when Nothing quickly. Clay's [rules](https://www.claymath.org/millennium-problems/rules/) require that a proposed solution be published in a qualifying outlet, that at least two years pass after publication, and that it receive "general acceptance in the global mathematics community" before the institute considers it. Martin Bridson, Clay's president, told AFP: "The process of evaluation is deliberately unhurried, and we shall ensure that it is absolutely rigorous." OpenAI has said it will not claim the prize, so for now the verdict rests with referees and with anyone willing to run the checker. Tao posted about the wider cost later on September 8. Good open problems, he wrote, are "now being mined in a non-renewable fashion," and "even the rumor of someone working on a problem can trigger a massive amount of AI-powered effort to flatten it before the original research project has time to reach its full potential." OpenAI's own timeline, from a rumor on September 1 to a certified theorem on September 6, is the clearest illustration on record. The Lean certificate lets anyone test whether the forced theorem holds. Whether it was the right theorem, and whose program it completed, are questions with no kernel to run them through. ## Sources - [OpenAI — On the Navier–Stokes Millennium Prize Problem (Sep 8, 2026)](https://openai.com/index/navier-stokes-solution/) - [GitHub — openai/NavierStokesAndEuler: Lean certificates for the Navier-Stokes and Euler results (Sep 8, 2026)](https://github.com/openai/NavierStokesAndEuler) - [Tristan Buckmaster — Statement on the Alpöge-Buckmaster results and contacts with OpenAI (Sep 8, 2026)](https://cims.nyu.edu/~tristanb/statement.pdf) - [Scientific American — AI may have just solved a million-dollar math problem. The field will never be the same (Sep 8, 2026)](https://www.scientificamerican.com/article/ai-may-have-just-solved-a-million-dollar-math-problem-the-field-will-never-be-the-same/) - [AFP via CTV News — OpenAI says AI solved one of math's hardest problems in days (Sep 8, 2026)](https://www.ctvnews.ca/sci-tech/article/openai-says-ai-solved-one-of-maths-hardest-problems-in-days/) - [Terence Tao — Open problems are being mined in a non-renewable fashion (Mathstodon, Sep 8, 2026)](https://mathstodon.xyz/@tao/117237320796901560) --- Canonical: https://www.thedeepfeed.ai/posts/2026-09-09-openai-navier-stokes-claim/ Site: https://www.thedeepfeed.ai Full corpus: https://www.thedeepfeed.ai/llms-full.txt