外力のない ℝ³ 上の3次元ナビエ＝ストークス方程式の解は、すべての時刻で滑らかなままか？（Clay の選択肢 A）

任意の粘性 ν > 0 と、ℝ³ 上の滑らかで発散が0、かつすべての導関数が多項式より速く減衰する初期速度 u₀ に対し、外力0のナビエ＝ストークス方程式が、ℝ³ × [0, ∞) で滑らかで運動エネルギーが一様に有界な解 (v, p) を持つかどうかを決定せよ。

Determine whether, for every viscosity ν > 0 and every smooth, divergence-free initial velocity u₀ on ℝ³ whose derivatives all decay faster than any polynomial, the Navier–Stokes equations with zero forcing have a solution (v, p) that is smooth on ℝ³ × [0, ∞) and has uniformly bounded kinetic energy.

Alternative (A) of the Clay Millennium Prize Problem. OpenAI's 2026-09-08 blowup construction (alternatives (C)/(D)) uses smooth external forcing and does not settle this unforced case, which formal-conjectures@fc2696b2 still records as open.

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

• Lean 4 formalization (formal-conjectures)

  形式証明

  到達状況

  未着手

  判定者

  the Lean 4 typechecker, against the pinned toolchain · 型検査

  定式化

  For every viscosity nu > 0 and every smooth, rapidly decaying divergence-free initial velocity on R^3, the unforced Navier-Stokes equations have a smooth solution with globally bounded kinetic energy.問いと同値Lean v4.33.1 + mathlib@0df444a3 (formal-conjectures@fc2696b2)検証対象を見る

  保たれているもの

  • The unforced case (f = 0)
  • Smoothness and the decay conditions on the initial data
  • The global-in-time energy bound

  加えられた仮定・条件

  • Fefferman's exact decay and energy conditions, encoded as Lean structures
  • The Clay errata's periodic-pressure convention in the sibling statement

  Statement only: the Lean file formalizes Fefferman's alternative, with `f := 0` for the unforced case. No proof is in the repository.

• 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

• Partial regularity of suitable weak solutions

  査読付きの証明

  到達状況

  進行中

  判定者

  the PDE community, through journal peer review · 査読

  定式化

  Shrink the possible singular set of a suitable weak solution until it is empty.問いより弱い

  保たれているもの

  • Works with the actual equation and the actual energy inequality

  弱まっているもの

  • Bounds the size of the singular set instead of excluding it: Caffarelli-Kohn-Nirenberg give one-dimensional parabolic Hausdorff measure zero, which is compatible with singularities existing

  加えられた仮定・条件

  • The notion of a suitable weak solution, with the local energy inequality

  閉じた道

  • Measure-zero statements cannot by themselves exclude a single blowup point; forty years of refinement have not closed the remaining gap.無条件
    • paperdoi:10.1002/cpa.3160350604L. Caffarelli, R. Kohn, L. Nirenberg, Partial regularity of suitable weak solutions of the Navier-Stokes equations, Comm. Pure Appl. Math. 35 (1982) 771-831

  証拠

  • paperdoi:10.1002/cpa.3160350604L. Caffarelli, R. Kohn, L. Nirenberg, Partial regularity of suitable weak solutions of the Navier-Stokes equations, Comm. Pure Appl. Math. 35 (1982) 771-831

• Conditional regularity criteria

  査読付きの証明

  到達状況

  進行中

  判定者

  the PDE community, through journal peer review · 査読

  定式化

  Prove that a solution staying bounded in a scaling-critical norm cannot blow up, then control that norm (Ladyzhenskaya-Prodi-Serrin; Escauriaza-Seregin-Sverak for L^infinity_t L^3_x).問いより弱い

  保たれているもの

  • Rules out blowup under a hypothesis that is exactly at the scaling threshold

  弱まっているもの

  • The hypothesis is not known to hold: the energy is supercritical in three dimensions, so nothing controls the critical norm

  加えられた仮定・条件

  • A critical-norm bound assumed, not proved

  閉じた道

  • Every known criterion is at or above the scaling-critical level, and the conserved energy sits below it. Closing that gap is the supercriticality problem itself, which the averaged-equation barrier says abstract methods cannot cross.無条件
    • paperarXiv:1402.0290T. Tao, Finite time blowup for an averaged three-dimensional Navier-Stokes equation, J. Amer. Math. Soc. 29 (2016) 601-674

  証拠

  • paperdoi:10.1070/RM2003v058n02ABEH000609L. Escauriaza, G. Seregin, V. Sverak, L^{3,infinity}-solutions of Navier-Stokes equations and backward uniqueness, Russian Math. Surveys 58 (2003) 211-250

• 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)

• 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 the unforced problem on R^3.問いとずれている

  保たれているもの

  • 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
• standardhttps://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdfC. L. Fefferman, Existence and Smoothness of the Navier–Stokes Equation, p. 2, alternative (A)

URI

https://atlasalt.com/q/2d5ef28e-0ed1-4904-aed9-60de439e0474

登録

2026-09-15

最終レビュー

2026-09-17

次回レビュー期限

2027-09-17

版

4315bb2c704b

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）