OpenAIのナビエ–ストークス証明主張、何が画期的で何が未確定なのか

OpenAIは、数学界にとって非常に大きな主張を公表しました。未公開の社内AIシステムが約1万の同時並行エージェントを動かし、3次元・非圧縮ナビエ–ストークス方程式の解が有限時間で特異点を起こすことを示す証明を見つけた、というものです。エージェント群の実行は約88時間、別のモデルによる証明支援系Leanでの形式化と検証にはさらに17時間かかったとされています。17

ただし、これは「解決が確定した」という意味ではありません。OpenAIは文章による証明とLeanの形式化資料を公開して外部の検討に委ねていますが、数学界での独立した受容や、クレイ数学研究所（CMI）の懸賞手続きには時間がかかります。126

OpenAIが「証明した」とする内容

ナビエ–ストークス方程式は、粘性をもつ流体の運動を表す方程式です。速度、圧力、粘性、流体自身の移流という非線形な効果を扱い、クレイの定式化では外力も許されています。焦点となるのは3次元で、十分に滑らかな初期状態から始めた流れが、未来永劫なめらかに保たれるのか、それとも有限時間で破綻し得るのか、という問題です。172133

OpenAIが述べる結果は、後者を示すブローアップ（有限時間特異点）構成です。静止状態から出発した流体に、滑らかでコンパクトな台をもつ外力を加えると、運動エネルギーは有界に保たれながら、速度が有限時間で無限大になる解が存在する、としています。134

平たくいえば、粘性があっても、3次元流体が数学的な意味で必ずしも「破綻しない」とは限らない、という主張です。これは激しい乱流を数値シミュレーションで見せたという話ではなく、解析的な証明として提示され、その論理展開をLeanで機械検査可能な形に落とし込んだものだとされています。134

正しければ、なぜ歴史的なのか

ナビエ–ストークス方程式の存在性と滑らかさは、CMIが2000年に提示した「ミレニアム懸賞問題」7題の一つです。賞金総額は700万ドルで、各問題に100万ドルが割り当てられています。1820

公式の問題設定には、大きく二つの到達点があります。所定の条件を満たす解が常に全時間で滑らかに存在することを示すか、あるいは許容される条件のもとで有限時間の破綻例を構成するかです。初期データだけでなく、外力にも条件が定められています。1721

OpenAIは、自らの構成が公式定式化のCとD、すなわちユークリッド空間と周期境界条件の設定における、滑らかな外力を伴う有限時間特異点の選択肢を確立すると主張しています。17 専門家による精査を通過し、公式の必要条件をすべて満たすと認められれば、ポアンカレ予想に続く2件目のミレニアム懸賞問題の解決となる可能性があります。OpenAIの発表時点では、残る6題は未解決とされていました。1118

Leanによる検証は重要だが、それだけで決着ではない

Leanは証明支援系です。定義、公理、すでに検証済みの定理に基づき、形式化された命題が論理的に導かれるかをチェックします。そのためLeanの検証成功は、Leanに与えられた形式化の範囲では論理的な穴がないことを示す有力な根拠になります。17

しかし、数学的な承認には専門家が次の点を検討する必要があります。

• 形式化された定理が、主張されるナビエ–ストークスの設定を正確に表しているか
• 論文の議論から形式的な定義への翻訳が適切か
• 仮定がクレイ問題の条件をすべて満たしているか
• 数学界全体が証明を受け入れるか

機械検証は、指定された形式的対象についての正しさを確認します。一方で、それが懸賞問題の意図する解釈と条件を完全に満たすかどうかまで、独力で判断するものではありません。

100万ドル賞がまだ授与されない理由

CMIは、提案された解答の直接投稿を受け付けていません。審査対象となるには、適格な媒体で公表され、公表から少なくとも2年が経過し、世界の数学界から一般的な受容を得る必要があります。26

したがって、OpenAIの証明が最終的に正しいと判明しても、直ちに賞金が授与される制度にはなっていません。現時点で正確なのは、「精査を受けている解決主張」あるいは「候補証明」という表現であり、受賞済みの成果と呼ぶ段階ではありません。126

決定的な論点：外力ありと外力なしは別の話

この発表をめぐる議論では、二つの問いが混同されがちです。一般向けに語られることの多い問いは、滑らかな外力なしの3次元流れが自発的に正則性を失うか、というものです。これに対し、OpenAIが説明する構成では、滑らかな外力を用いています。3435

この差は科学的には重要です。ただし、外力を使うことだけでクレイの枠組みから外れるわけではありません。公式定式化には、滑らかで急減衰する外力を含む選択肢があるためです。1735 賞の対象になるかを左右するのは、より狭い通俗的な問いに一致するかではなく、OpenAIの証明が該当する公式選択肢の条件を一つ残らず満たすかどうかです。

優先権と学習データを巡る論争

発表の前後には、ニューヨーク大学の数学者Tristan Buckmasterと、Anthropic所属のLevent Alpögeに関わる研究もありました。両者の仕事は、標準的なナビエ–ストークス問題の解決として確立されたものではなく、外力を含む関連する流体方程式を扱うものでした。237

Buckmasterは、OpenAIが共同発表の枠組みを提案する際、Anthropicに所属するAlpögeを外そうとしたと主張しました。また、Codexを含むOpenAI製品上での研究上のやり取りが、モデル学習に寄与していた可能性についても疑問を呈しました。25052

OpenAIは、この問題の解決にあたり、同社の研究者やAIエージェントが2人の具体的な研究内容や利用者データにアクセスしていないと述べています。その一方で、製品利用から得られた匿名化データがモデル改善に役立った可能性までは完全に否定できない、としています。5354

ここには未解決の点が残ります。関連するやり取りが学習対象になり得たのか、実際に利用されたのか、そして結果に実質的な影響を与えたのかは、公開報道だけでは確定していません。OpenAIがBuckmasterとAlpögeの研究を利用したとする確立した証拠はなく、疑惑を事実として扱うべきではありません。25354

今後、注目すべきこと

評価の決め手は、AIエージェントの数や計算時間ではありません。独立した専門家が原稿とLeanの形式化を精査し、形式検証を再現し、その定理がクレイ問題の該当条件を満たすと合意できるかどうかです。

それが実現すれば、今回の発表は数学研究とAI支援研究の双方で画期となる可能性があります。それまでは、重大で公開済みの候補証明として捉えるのが妥当です。同時に、研究の優先権、データガバナンス、そしてAI企業が未公表の研究アイデアをどう扱うべきかという別の論争も、なお決着していません。12653