この記事の日本語版はまだありません。英語版を表示しています。

Navier–Stokes: OpenAI's claim of finite-time blowup with smooth forcing

OpenAI claims an internal model proved that a 3D incompressible fluid starting at rest can develop a singularity in finite time under a smooth external force, one of the four forms of the Millennium Prize problem; the 166-page proof is unverified and its priority is disputed.

問題
Can solutions of the 3D incompressible Navier–Stokes equations break down in finite time? (Clay statements C and D: breakdown on R3\mathbb{R}^3 and on the torus with a smooth force)
貢献
OpenAI internal model, with GPT-6 Astra for the Lean formalization · About 10,000 concurrent agents over about 88 hours, per OpenAI
検証
Lean formalization by OpenAI (its fidelity is disputed)
経緯
Result reached 2026-09-05 → announced 2026-09-08 → Clay note 2026-09-11
出典
OpenAI announcementManuscript (166 pages)Clay Mathematics Institute noteCritique of the Lean proof (arXiv:2610.08144)Statement by Tristan Buckmaster
未検証Unverified · priority disputed

The problem

The Clay Mathematics Institute's Millennium Prize problem on the Navier–Stokes equations can be won by proving any one of four statements: global regularity on R3\mathbb{R}^3 (A) or on the torus (B), or breakdown on R3\mathbb{R}^3 (C) or on the torus (D). The breakdown statements allow a smooth external force.

What AI did

On 8 September 2026 OpenAI announced that a new internal model had shown that an initially smooth fluid, starting at rest, can develop a singularity in finite time under a smooth external force, with finite energy throughout. This is a blowup result, not global regularity; OpenAI says it establishes statements C and D. According to OpenAI, about 10,000 concurrent agents reached the result on 5 September after about 88 hours, and GPT-6 Astra then took 17 hours to formalize it in Lean. OpenAI also claims an unforced blowup for the Euler equations, and says it will not claim the prize.

How it was checked

The Clay Institute's note of 11 September says the problem "has apparently been settled" and describes its process as "deliberately unhurried"; it has not accepted the result. A paper of 6 October (arXiv:2610.08144) argues that the Lean proof does not correspond to the written proof, citing mistranslations, though it does not claim the result is false. Javier Gómez-Serrano told NPR that "the community seems to have the consensus that it is correct", and also that "the paper is not written for humans".

Limitations

The result relies on the smooth, unphysical external force that Clay's statements C and D allow. Priority is disputed: Tristan Buckmaster and Levent Alpöge obtained forced smooth blowup for related equations (including 3D Euler) in August with heavy use of AI, and Buckmaster alleges that OpenAI had prior knowledge of their work; OpenAI denies that his prompts could have influenced its system and credits them with priority for forced Euler. Until the proof is checked independently, we grade it "unverified".

∎