# OpenAI Claims an Internal Model Resolved Navier-Stokes, and Mathematicians Are Contesting It

The company says roughly 10,000 parallel agents worked 88 hours to produce a finite-time singularity proof formalized in Lean, while the Clay Mathematics Institute still lists the problem as open.

- Published: 2026-09-09T06:20:57.202Z
- Canonical: https://polylog.news/ai/2026-09-09/openai-claims-an-internal-model-resolved-navier-stokes-and-m
- Publisher: Polylog (AI desk)
- Section: tech
- Sources: [OpenAI](https://openai.com/index/navier-stokes-solution), [Polylog editors](https://polylog.news)

OpenAI said on September 8 that an unreleased internal system, one it describes as more capable than the GPT-6 Astra model it previewed five days earlier, produced a solution to the Navier-Stokes Millennium Prize Problem. The company [published a writeup together with a formal proof in Lean](https://openai.com/index/navier-stokes-solution), the proof assistant that mechanically checks each logical step. The claimed result is a finite-time singularity: a smooth fluid flow that breaks down after a finite interval. The Clay Mathematics Institute problem admits either a regularity proof or a demonstration that solutions can fail, so a verified blowup construction would settle it.

The production details are what practitioners should note. [Reporting on the announcement](https://www.quantamagazine.org/ai-has-solved-one-of-maths-1-million-millennium-prize-problems-20260908/) puts the run at about 88 hours with as many as 10,000 agents in parallel and a 165-page writeup, a scale of computation closer to a sustained research campaign than a single chat session. [Telegram channel AI Post carried the same figures](https://t.me/aipost/8089) to Russian and English-language AI audiences within hours.

Two things are disputed. First, status: the Clay Mathematics Institute continues to list Navier-Stokes among its unsolved problems, and independent mathematicians have not yet published a confirmation that the released Lean artifact compiles and proves the stated theorem. Second, credit. Tristan Buckmaster of New York University and Levent Alpöge of Anthropic released Lean-verified blowup proofs for related fluid systems, and Buckmaster has alleged that private Codex-session work may have been visible to OpenAI researchers. OpenAI says it finished its own Lean verification on September 6 without accessing that work, and Sébastien Bubeck of OpenAI [called the allegations false and inflammatory](https://www.scientificamerican.com/article/openai-claims-blockbuster-math-breakthrough-amid-swirl-of-controversy/).

The unusual feature of this dispute is that one half of it is decidable. Originality claims are a matter of testimony, but a Lean file either type-checks under the standard axioms or it does not, and any mathematician with the artifact can run that check.

## What this means

Formal verification shifts the constraint on AI-produced mathematics away from years of human refereeing and toward whether a lab releases the machine-checkable artifact. If outside mathematicians compile OpenAI's Lean proof successfully, the claim stands on its own regardless of the credit dispute, and every lab gains an incentive to route hard research claims through proof assistants. If the artifact stays partly withheld, the result remains a vendor assertion, and OpenAI absorbs the reputational cost. Either way the run itself is a demand signal: 10,000 concurrent agents for 88 hours is sustained accelerator consumption for a single question, which supports the case that frontier inference spending grows faster than chat usage alone would justify.

## What to watch

- Whether mathematicians outside OpenAI report compiling the Lean formalization and confirm it proves the stated theorem, which is the difference between a verified result and a press release.
- Whether the Clay Mathematics Institute changes the problem's listed status or comments on the submission, the clearest external signal of acceptance.
- Whether other labs start attaching Lean or comparable machine-checked artifacts to research claims, which would set a new evidentiary norm for AI-generated science.