OpenAIがナビエ・ストークス証明を公開、賞金100万ドルの難問

OpenAIの公式発表と懸賞のルールから、数学成果の扱いを紹介します。証明の主張、形式検証、専門家による検討を分けて整理します。

1万体のAIエージェントが88時間で証明を構築

ナビエ・ストークス方程式は、水や空気といった流体の動きを記述する方程式です。「なめらかな初期状態から出発した流体が、有限の時間内に速度が無限大になる特異点(破綻)を起こしうるか」が90年近く未解決で、クレイ数学研究所が2000年に選定した7つの「ミレニアム懸賞問題」の一つとして100万ドルの賞金が用意されています。OpenAIは公式ブログで、「粘性がどんな正の値であっても、静止状態から出発し運動エネルギーは有限に保ったまま有限時間で速度が無限大になる流れを構成できる」ことを示す証明を発表しました。証明は165ページの論文にまとめられ、一行ずつコンピュータが検証できる形式検証言語「Lean」でのチェックも完了しています。使われたのは既存の「GPT-6 Astra」より大幅に高性能な未公開の内部モデルで、これを土台に最大約1万体のAIエージェントが並行作業し、証明にたどり着くまで約88時間、Leanでの形式検証にさらに17時間かかりました。やり取りされたメッセージは270万件、出力トークンは約1,300億に上り、計算コストは「数百万ドル規模」になるとOpenAIのセバスチャン・ビュベック氏は見積もっています。

賞金は請求せず、フェルマー証明とは中身が違う

OpenAIは公式ブログで「私たちはこの成果でミレニアム賞を請求するつもりはない」と明言し、発表の狙いは「AIモデルの大きな進歩を報告すること」にあると述べています。そもそもクレイ数学研究所の公式ルールでは、解決と認められるには査読付き発表・発表から2年以上経過・数学界での広い受け入れの3条件が必要で、今回はまだこの「定着期間」を経ていません。数日前に話題になったAnthropicのClaudeによるフェルマーの最終定理の形式化とは、挑んだ中身もAIの使い方も異なります。

OpenAIは公式ブログで、AnthropicのLevent Alpöge氏らが関連する「強制オイラー方程式」に取り組んでいるという噂を耳にしたことが今回のきっかけだったとも明かしており、数学の難問にAIを投入する動きは両社で同時並行に進んでいるようです。

OpenAIは、主張の妥当性を専門家が確認する体制として、数学者による独立諮問組織の設置も発表しています。

まとめ：証明の主張と検証の段階を区別する

AIによる数学研究の動向を調べる方には、証明の公開・形式検証・数学界での受容を区別することが重要です。未公開モデルと大規模な計算資源による成果を、通常サービスの再現性とはみなせません。何が確認済みで、何が今後の検証に残るかに着目するとよいでしょう。