OpenAI、ナビエ・ストークス方程式を証明したと発表 論争に

OpenAI は 9 月 8 日、社内モデルがミレニアム懸賞問題の一つ、ナビエ・ストークス方程式の解の存在性と滑らかさに関する証明を生成したと発表した。この方程式は、浴槽の排水口にできる渦から飛行機の翼まわりの空気の流れ、血管内の血流に至るまで、流体の運動を記述する基本方程式であり、200 年以上研究されてきたにもかかわらず、あらゆる初期条件のもとで解が常に滑らかであり続けるかどうかは分かっていなかった。OpenAI によれば、同社のモデルは特定の条件下で、方程式の解が有限時間内に無限大へと発散する、いわゆる「ブローアップ」現象が起こることを証明したという。この問題はクレイ数学研究所が 100 万ドルの懸賞金を懸けたミレニアム懸賞問題の一つだが、OpenAI が証明したのは強制項を含む変形版であり、懸賞の対象基準には該当しないとして、同社は賞金を請求しないとしている。

1万個のAIエージェントが88時間で

OpenAI によると、今回の証明は社内モデルが約 1 万個の AI エージェントを並行して動員し、約 88 時間で完成させたもので、その後、形式証明言語 Lean によって検証済みだという。この発表の直前、ニューヨーク大学の数学者トリスタン・バックマスターは、Anthropic に所属する数学者レベント・アルプージェとともに、ナビエ・ストークスよりも単純な形のオイラー方程式で同種のブローアップ現象を証明したとSNS上で公開していた。バックマスターはその後の声明で、自分たちの研究の進展に関する噂を耳にした OpenAI が、同じ手法を採用してナビエ・ストークス方程式にまで証明範囲を広げたと主張した。彼は、OpenAI の研究者セバスチャン・ビュベックとの電話で、アルプージェを Anthropic 所属という理由で著者リストから外すか、OpenAI が単独で結果を発表するかの二択を提示されたと述べている。

OpenAI の反論と数学者たちの懸念

OpenAI のビュベック研究員はこの主張を強く否定した。同社の社内モデルはバックマスターとアルプージェの研究資料を見たことがなく、オイラー方程式に対する OpenAI のアプローチは 2 人の手法と根本的に異なると説明した。ただし、ナビエ・ストークス方程式に関する最終的な証明については、2 人が用いた手法に近い経路をたどったことは認めている。OpenAI は公式発表の中で、2 人の研究を公開前に閲覧したことはなく、特定のユーザーデータを証明に利用したこともないと述べた一方で、2 人が同社の製品を利用する中で生成された非識別化データが、間接的にモデルの性能向上に寄与した可能性までは否定していない。OpenAI の最高経営責任者サム・アルトマンも SNS 上で、事前の調整がもっとうまくいっていればよかったと述べ、遺憾の意を示した。

• 発表日:2026年9月8日
• 証明の方法:AI エージェント約 1 万個、計算時間は約 88 時間
• 検証ツール:形式証明言語 Lean
• 先行チーム:バックマスター(ニューヨーク大学)とアルプージェ(Anthropic)がオイラー方程式のブローアップを先に証明
• ミレニアム懸賞金:クレイ数学研究所の100万ドル、今回の証明は対象外

この一件は単なる先取権争いにとどまらない注目を集めている。数学者トリスタン・バックマスターは、1997 年に IBM のスーパーコンピューター「ディープ・ブルー」がチェス世界チャンピオンのガルリ・カスパロフを破った瞬間になぞらえ、学界は今こそ AI の役割について慎重かつ真剣な議論を始めるべきだと述べた。シドニー大学の数学者ズザンナ・ダンショは、OpenAI の対応が、出典を明らかにし共同研究者を認めるという数学界の基本的な倫理原則に反していると指摘した。何より、この証明はまだ独立した査読を経ていないため、実際に検証された成果なのか、それとも発表効果を狙った主張なのかという根本的な問いは、依然として未解決のままだ。

日本の数学研究にとって、今回の一件は企業発表の速さが査読に代わるものではないことを示している。Lean などを用いた形式検証に取り組み始めている国内の大学や研究機関は、AIによる証明を対外的に発表する前に、著者権や学習データの出所に関する明確なルールを整える必要がある。それこそが、OpenAI と Anthropic の間で今起きているような対立を避ける唯一の方法だろう。