【geek-terminalニュース】OpenAIのNavier-Stokes証明AIと検証論争の最新情報

以前お伝えした未解決数学問題・証明検証テーマの続報です。今回の主役は、ついに具体名が出たNavier-Stokes存在と滑らかさ問題です。ただし本丸は「AIがミレニアム問題を解いたのか」という見出しの派手さだけではありません。もっとギークに刺さるのは、AIが生成した証明を誰が、どの形式体系で、どの査読プロセスに乗せ、どこまで人間の数学として認めるのか。そしてその裏側で、研究者の未公開作業、クラウドAIへの入力、企業間競争、著者性がどう衝突するのかです。

【事象の全貌と背景】

OpenAIは2026年9月8日、内部AIシステムがNavier-Stokes Millennium Prize Problemの解を生成し、解析的証明とLean形式化を共有したと発表しました。公式説明によれば、主張の中身は3次元非圧縮流体について、滑らかな初期状態と滑らかな外力のもとで有限時間に特異点が形成される、というものです。OpenAIはこれがClay Mathematics Instituteの定式化におけるCおよびDを確立し、Millennium問題を解決すると述べています。一方で、賞金を請求する意図はないとも明記しています。

ここで重要なのは、これは単なる「すごいAIニュース」ではなく、数学の信用生成プロセスそのものを揺さぶる話だという点です。Navier-Stokes問題は、流体運動を記述する基礎方程式について、滑らかな解が常に存在し続けるのか、それとも有限時間で速度が無限大に発散するような特異点が生じうるのかを問う未解決問題です。OpenAIは、航空機設計、天気予報、血流研究などにも関係する基礎理論だと説明しています。

加えて今回は、並行研究の存在が火種になっています。OpenAIは、9月1日に2つのMillennium問題が解かれたという噂を聞き、未解決Millennium問題を評価する取り組みを始めたと説明しています。その後、その噂がLevent AlpögeとNYU教授Tristan Buckmasterに関係していたと理解し、9月6日の完成後に両者へ連絡したとしています。OpenAI側は、両者の成果が強制Euler問題の解決だったと知り、その優先権を認めた、と公式に述べています。

【技術的ディープダイブ】

OpenAIの公式発表で確認できる数値はかなり異常です。使用したのはGPT-6 Astraより大幅に高性能だとされる内部モデルで、キャッシュされたインターネット閲覧とコード実行などのツールを持つ協調エージェント群を使ったとされています。Navier-Stokes解を出したグループは約1万の同時エージェント規模で、エージェント開始から約88時間後の2026年9月5日に解へ到達し、9月6日にGPT-6 AstraによるLean形式化・検証を完了したとOpenAIは説明しています。全問題を通じて490万メッセージ、約3000億出力トークン。Navier-Stokesだけでも270万メッセージ、約1300億出力トークンという、もはや人間の研究会ではなく分散探索クラスタに近いスケールです。

技術的な主張も興味深い。OpenAIは、解を内側へ螺旋しながら細長くなる渦として描写しています。中心領域が縮小し、速度が増大していく一方、エネルギーは有限に保たれる。加速度、圧力勾配、運動量輸送、粘性などの項が大きくなりながらも精密に打ち消し合い、速度場が無限大へ向かうのに外力は滑らかなまま、という構造です。数学的には、ただ発散する例を作ればよいわけではなく、Clayの条件に沿って滑らかさ、エネルギー、外力、方程式の整合性をすべて守る必要があります。

また、OpenAIはまず粘性項を除いたEuler方程式の正則性問題を「より容易な問題」として試し、100弱のエージェントが約50時間で非外力Euler正則性の反証を作ったと述べています。その後、他のMillennium問題から計算資源をNavier-Stokesへ移し、Codexで複数エージェント群の有用な洞察を統合した、という流れです。ここでLean形式化が出てくる意味は大きい。AIが自然言語でそれっぽい証明を書く時代から、機械検査可能な形式証明へ寄せることで、幻覚と本物の差分を狭めようとしているからです。ただし、Leanで検証されたとされる範囲が数学コミュニティにどう評価されるかは、今後の精査対象です。

【コミュニティの生々しい熱量と議論】

Redditのr/singularityでは、OpenAI公式発表へのリンクを中心に、内部モデルがGPT-6 Astraより強い点や「1週間前にGPT-6が出たばかり」という速度感への反応が目立ちました。別スレッドでは、IMO金メダル級からMillennium問題へ1年未満で進んだという認識や、Leanで数学証明を検査できることへの期待、2027年にはさらに多くの未解決問題が解かれるのではという憶測も共有されています。ここはかなり加速主義的で、「数学研究のスループットが桁違いに変わった」という読みが強い空気です。

一方でr/MachineLearningとr/LocalLLaMAは、かなり温度が違います。r/MachineLearningでは、Tristan BuckmasterとLevent Alpögeの未公開作業がOpenAIの結果に影響した可能性や、OpenAIの「匿名化データがモデル改善に役立った可能性は低いが排除できない」という趣旨の記述への疑念が議論されています。r/LocalLLaMAでは、研究者がCodexに草稿を投入していたこと、OpenAIが近い時期に同種の解を出したこと、非公開チャットが訓練に使われたかへの回答が明確でなかったとする投稿を起点に、クラウドLLMへ未公開研究を入れるリスクが論点化しました。

Hacker News側の反応は、さらに生々しいです。あるユーザーは「両側の文脈が欠けていて、自分の分野ではないので誰か解きほぐしてほしい」という慎重な姿勢を示しています。別のユーザーは、OpenAIが同じ問題に取り組んでおり、公開タイムラインで合意できなかったため研究者側が先に出した、という背景を整理しています。さらに強い反応として、Buckmaster側の文章を引用しながら、「forced」という方向性が偶然数日で出るものなのか、OpenAI内部でどれだけ人間の入力や計算資源が使われたのか、Codexセッションが訓練やアクセスに関係したのかが疑問視されています。ただし、ここは重要で、これらはコミュニティ上の疑惑や当事者主張を含む議論であり、公式に確定した事実としては扱えません。

The Decoderは、BuckmasterがOpenAI研究者からAnthropic所属のAlpögeを共著から外すよう圧力を受けたと主張している、と報じています。同時に、OpenAI側が疑惑を否定し、公開前に両者の作業を見ておらず、OpenAIの解はBuckmaster・Alpögeのアプローチと根本的に異なると説明したことも報じています。つまり現時点で断定できるのは、OpenAIが解とLean形式化を公開したこと、並行研究者との接触と優先権認知を説明していること、そして外部では研究倫理・データ利用・著者性をめぐる疑義が噴出していることまでです。

【今後の展望とエコシステムへの影響】

もしOpenAIの証明が数学コミュニティの精査、形式検証、査読を通って受け入れられるなら、これはAI研究史だけでなく数学史の転換点になります。しかし、より現実的なインパクトは「未解決問題が解けたか」より先に、「AIが出した証明を受理するパイプライン」が必要になることです。自然言語の論文、Leanなどの形式化、専門家査読、優先権の記録、使用データの監査、クラウドAIに投入された未公開研究の扱い。この全セットが、今後の数学研究インフラになります。

オワコン化しそうなのは、単純なベンチマークの点数だけでAIの数学能力を語る態度です。IMOで何点、定理証明ベンチで何問、という話はまだ重要ですが、今回のレベルでは「どれだけのエージェントを並列に走らせ、どの中間結果を統合し、どの証明支援系で検査し、どの部分を人間が信用するのか」が本体になります。AI数学は、モデル単体の知能評価から、研究OS、証明コンパイラ、査読プロトコル、監査ログの競争へ移ります。

そして企業利用の観点では、クラウドLLMに未公開の証明、特許、論文草稿、実験ノートを入れることのリスク評価が一段厳しくなります。OpenAIは特定ユーザーデータが解決にアクセスされていないと主張していますが、匿名化データ由来のモデル改善可能性を低いが排除できないと書いたことで、研究者コミュニティの不安はむしろ具体化しました。今後は、研究用AI環境において、ゼロ保持、学習不使用、監査可能な隔離実行、オンプレミスまたはローカルLLMとの使い分けが強く求められるはずです。

今回のNavier-Stokes騒動は、AIが数学者を置き換えるという単純な話ではありません。むしろ、数学者、形式検証エンジニア、AI企業、査読者、コミュニティが同じ証明オブジェクトをめぐって衝突する時代の始まりです。答えそのものよりも、答えが信用になるまでの経路が問われている。Geek Terminal的に言えば、これは「AIがミレニアム問題を解いたか」ではなく、「数学のCI/CDが必要になった瞬間」です。