ナビエ＝ストークス方程式の解の存在と滑らかさ：Clay の選択肢 (A)〜(D) のいずれかを証明できるか？（ミレニアム懸賞問題）

粘性 ν > 0 の3次元非圧縮ナビエ＝ストークス方程式について、Fefferman による Clay 研究所の公式問題文にある4つの選択肢のいずれかを証明せよ。(A) ℝ³ 上で外力なしの解が大域的に存在し滑らかである。(B) ℝ³/ℤ³ 上で同様。(C) ℝ³ 上で、滑らかで減衰する初期値と外力であって、大域的に滑らかな有限エネルギー解を持たないものが存在する。(D) ℝ³/ℤ³ 上で同様の破綻が起きる。

Prove one of the four alternatives in Fefferman's official Clay problem statement for the incompressible Navier–Stokes equations in three space dimensions with viscosity ν > 0: (A) global existence and smoothness of unforced solutions on ℝ³; (B) the same on ℝ³/ℤ³; (C) existence of smooth, decaying initial data and forcing on ℝ³ with no global smooth finite-energy solution; (D) the same breakdown on ℝ³/ℤ³.

One of the seven Clay Millennium Prize Problems. On 2026-09-08 OpenAI announced a proof of alternatives (C) and (D), with a paper ("Finite Time Blowup for Navier–Stokes", https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf) and a Lean 4 formalization (https://github.com/openai/NavierStokesAndEuler/commit/8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538). formal-conjectures@fc2696b2 records (C) and (D) as solved with that formal proof, and (A) and (B) as open. As of 2026-09-15 the Clay Mathematics Institute has not accepted the result and still lists the problem as unsolved; independent review is pending. Open points raised publicly: whether the forced construction matches the intent of the problem (the unforced cases (A)/(B) remain open), and a priority dispute raised by T. Buckmaster.

解決したかどうかは、問いではなくアプローチごとに決まります。Atlas は判定しません。外部の判定者が何をしたかを記録します。

• Forced breakdown, alternatives (C) and (D)

  査読付きの証明

  到達状況

  解決と判定

  判定者

  the Lean 4 typechecker for the published formalization; the Clay Mathematics Institute and the research community for whether it settles the prize problem · 型検査

  定式化

  Construct smooth initial data and smooth forcing on R^3 (and on the torus) for which no global smooth finite-energy solution exists, i.e. Fefferman's alternatives (C) and (D).問いと同値Lean v4.33.1 + mathlib@0df444a3 (formal-conjectures@fc2696b2)検証対象を見る

  保たれているもの

  • One of the four alternatives Fefferman's problem statement asks for, in full
  • Three space dimensions, positive viscosity, smooth data

  弱まっているもの

  • Settles the prize question through the forced alternatives; the unforced alternatives (A) and (B), which most of the field treats as the substance of the problem, remain untouched

  加えられた仮定・条件

  • Smooth external forcing, which the problem permits but does not require

  Atlas has not rebuilt the Lean proof. The record rests on the published formalization and on formal-conjectures marking both statements solved. The Clay Mathematics Institute has not accepted the result.

  閉じた道

  • The construction uses smooth external forcing. It says nothing about the unforced alternatives (A) and (B), which are tracked here as separate questions.無条件
    • standardhttps://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdfC. L. Fefferman, Existence and Smoothness of the Navier-Stokes Equation, p. 2 (alternatives A-D)

  証拠

  • repositoryhttps://github.com/openai/NavierStokesAndEuler@8937a8f4cbc7abaab5e9e97d1cc7f5d2319d9538Lean 4 formalization of alternatives (C) and (D)
  • preprinthttps://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdfOpenAI, Finite Time Blowup for Navier–Stokes (2026-09-08)
  • repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Millennium/NavierStokes.lean:288-310 (navier_stokes_breakdown_R3 and navier_stokes_breakdown_periodic marked solved, formal_proof linked to the commit above)

• Abstract energy methods

  閉じた道（障壁）

  到達状況

  この道では到達できないと証明済み

  判定者

  none: the obstruction is a published theorem about a model equation, not a decision procedure · 引用

  差分（このアプローチが問いの何を保ち、何を弱めるか）はまだ書かれていません。人類審査で書きます。

  閉じた道

  • Tao constructs finite-time blowup for an averaged Navier-Stokes equation that satisfies the same energy identity and the same function-space estimates as the true equation. Any argument that uses only upper bounds on the nonlinearity plus the energy identity therefore cannot prove global regularity: it would prove it for the averaged equation too, where it is false.無条件
    • paperarXiv:1402.0290T. Tao, Finite time blowup for an averaged three-dimensional Navier-Stokes equation, J. Amer. Math. Soc. 29 (2016) 601-674

• Uniqueness in the weak class (convex integration)

  閉じた道（障壁）

  到達状況

  この道では到達できないと証明済み

  判定者

  none: the obstruction is a published theorem · 引用

  差分（このアプローチが問いの何を保ち、何を弱めるか）はまだ書かれていません。人類審査で書きます。

  閉じた道

  • Buckmaster and Vicol construct distinct finite-energy weak solutions with the same initial datum, so weak solutions of 3D Navier-Stokes are not unique in that class. The route 'prove regularity by establishing uniqueness among finite-energy weak solutions' is closed.無条件
    • paperdoi:10.4007/annals.2019.189.1.3T. Buckmaster, V. Vicol, Nonuniqueness of weak solutions to the Navier-Stokes equation, Ann. of Math. 189 (2019) 101-144 (arXiv:1709.10033)

• Unforced global regularity

  査読付きの証明

  到達状況

  未着手

  判定者

  the PDE community, through journal peer review · 査読

  定式化

  Settle the prize problem through alternative (A) or (B): prove global smoothness for unforced data.問いより強い

  保たれているもの

  • Would answer the question in the direction the field treats as its substance

  弱まっているもの

  • Nobody has a route: this is the open case, tracked as two separate questions in Atlas

  加えられた仮定・条件

  • Nothing

  閉じた道

  • The energy is supercritical in three dimensions, and abstract energy-based methods are ruled out by the averaged-equation barrier.無条件
    • paperarXiv:1402.0290T. Tao, Finite time blowup for an averaged three-dimensional Navier-Stokes equation, J. Amer. Math. Soc. 29 (2016) 601-674

• Numerical search for self-similar blowup

  計算による判定

  到達状況

  進行中

  判定者

  execution: a numerical solution can be recomputed, but it does not decide the mathematical statement · 実行

  定式化

  Find approximate self-similar blowup profiles numerically and, from them, build a computer-assisted proof for either alternative.問いとずれている

  保たれているもの

  • Points at where a singularity would have to look like, guiding the analysis

  弱まっているもの

  • Numerics do not adjudicate: finite resolution cannot distinguish blowup from very fast growth

  加えられた仮定・条件

  • The published constructions are for the Euler, Boussinesq and porous-media equations, or for Navier-Stokes with boundary, not for the smooth unforced Navier-Stokes question

  閉じた道

  • A numerical profile is evidence, not a proof; converting one into a theorem requires a separate computer-assisted argument with rigorous error control.無条件
    • paperdoi:10.1073/pnas.1405238111G. Luo, T. Y. Hou, Potentially singular solutions of the 3D axisymmetric Euler equations, PNAS 111 (2014) 12968-12973

  証拠

  • paperdoi:10.1073/pnas.1405238111G. Luo, T. Y. Hou, Potentially singular solutions of the 3D axisymmetric Euler equations, PNAS 111 (2014) 12968-12973
  • preprintarXiv:2509.14185Discovery of Unstable Singularities (Google DeepMind, NYU, Stanford and others, 2025): new unstable self-similar blowup families for the incompressible porous media, Boussinesq and 3D Euler equations

• repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Millennium/NavierStokes.lean:271-310
• standardhttps://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdfC. L. Fefferman, Existence and Smoothness of the Navier–Stokes Equation, p. 2 (alternatives A–D)

URI

https://atlasalt.com/q/0ea2619f-b33b-47cc-81ba-d8fec8e275b2

登録

2026-09-15

最終レビュー

2026-09-17

次回レビュー期限

2027-09-17

版

78084fab2502

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）