AIが90年の難問に「答え」を出した — 1万体の協働と、解決認定まで残る最低2年の壁

深堀AI・イノベ2026-09-09

執筆: KID

【科学・AI】連載・AI・イノベ【国際・海外企業】米国【経済・生成AI】

#AI#OpenAI#数学研究#Navier–Stokes方程式#Lean#形式証明#マルチエージェント#科学研究

AIが90年の難問に「答え」を出した — 1万体の協働と、解決認定まで残る最低2年の壁

AIが数学者の補助をする段階から、未解決問題の証明そのものを大量のAIが探し、別の仕組みで書き直して検査する段階へ進みました。

OpenAIは2026年9月8日、流体の動きを表すNavier–Stokes方程式について、有限時間で速度が際限なく大きくなる例を構成したと発表しました。
同社は人が読める数式による証明をまとめた論文と、定理証明支援系Leanで形式化したコードを公開しています。
主張どおりなら、2000年に100万ドルの賞金が設定されたミレニアム懸賞問題の一つに答えが出たことになります。

ただし、発表日と「解決が確定した日」は同じではありません。ここで起きた本当の変化は、難問の答えが確定したことより先に、研究の探索速度と検証の組み方が大きく変わったことです。

90年の難問に、88時間で一つの構成を示した

証明が扱うのは、滑らかに始まった流体の計算が、ずっと滑らかなまま続くのかという問いです。 Navier–Stokes方程式は航空機の設計、天気予報、血流の解析などで使われます。
方程式自体は19世紀からありますが、3次元の流れが必ず滑らかに続くかは、およそ90年にわたり決着していませんでした。

OpenAIの論文は、初めは静止している流体へ、外力（流体の外から加える力）を空間と時間の限られた範囲で滑らかに加える構成です。
流体全体の運動エネルギーは有限のままなのに、ある場所の速度が有限時間で無限に大きくなると示します。
現実の水が無限の速さになるという意味ではありません。
連続した流体として扱う数式の表現が、その時点で破綻するという意味です。

公開論文は165ページあります。
OpenAIは、Clay Mathematics Instituteが定めた公式問題の選択肢CとD、すなわち外力を伴う全空間と周期空間での破綻例を示したと説明しています。
論文冒頭の定理も、粘り気がゼロでないあらゆる場合について、滑らかな外力と初期値から速度が際限なく大きくなる解を構成する形です。

AI群が作業を始めてから結果へ到達するまでは約88時間、Leanによる形式化と検証には追加で17時間かかりました。
人間が長く積み上げてきた数学を短期間で置き換えた、という話ではありません。
過去の理論、公開資料、問題設定を読み込んだ探索系が、膨大な候補を並行して試せるようになった出来事です。

1万体が探索し、別のAIが証明を固めた

今回の成果は、賢いAIへ一度質問して返ってきた答えではありません。 OpenAIは新しい社内モデルを使い、規模や役割の異なるエージェント群を走らせました。
Navier–Stokes問題を担当した系は、およそ1万体のエージェントが同時に動く規模だったとしています。

各グループには、滑らかさを証明する方向と、破綻例を作る方向の異なる問題設定を与えました。
近い問題であるEuler方程式（粘り気を表す項を除いた流体の式）の結果が得られると、その知見をNavier–Stokes側へ渡し、有望な方向へ計算資源を寄せています。
途中の成果をまとめ直し、別グループへ受け渡す役割にはCodexも使われました。

Navier–Stokesだけで、やり取りは270万件、出力は文章の細かな単位で約1300億トークンです。
全問題では490万件、約3000億トークンに達しました。
これは一つの長い思考ではなく、多数の探索を走らせ、有望な枝だけを残し、最後に一貫した証明へ圧縮する工程です。

ここから研究開発のボトルネックも変わります。
モデルの一問一答の正答率だけでなく、どの仮説へ資源を振るか、途中結果をどう共有するか、誤った枝をどこで切るかが成果を左右します。
AIの性能比較が「1体の試験点数」から「研究組織として何を完成させられるか」へ広がったわけです。

Leanが確かめる範囲と、外に残る三つの確認

Leanの検査を通ったことは強い証拠ですが、それだけで懸賞問題の認定が終わるわけではありません。 Leanは、登録された定義と公理から結論まで、推論規則に反していないかを細かく確認します。
手書きの証明で起きやすい「ここは明らか」と飛ばした部分を埋め、同じコードを第三者が動かせる利点があります。

一方で、外側には少なくとも三つの仕事が残ります。
第一に、形式化した定義がClayの公式問題と本当に一致するか。
第二に、紙の論文で説明する構成とLean上の定理が同じ数学を表しているか。
第三に、証明の新規性や研究上の帰属をどう整理するかです。
コードが動くことと、科学共同体が成果全体を受け入れることは別の判定です。

Clayの規則はさらに明確です。
同研究所は提案された解答を直接受け付けません。
適格とされる媒体へ掲載され、そこから最低2年が経過し、世界の数学界で一般的に受け入れられることが、審査を始める条件です。
OpenAI自身も、今回の結果で賞金を請求する意図はないと明記しています。

発見の経緯には未確定の論争もあります。
ニューヨーク大学のTristan Buckmaster氏とAnthropicのLevent Alpöge氏は、近いEuler方程式の研究を進めていました。
Buckmaster氏は、OpenAIがその進展を知った後に関連する方向へ資源を集中させたと主張しています。
OpenAIは、公開前のプロンプトや証明へアクセスしておらず、両者の研究を使っていないと否定しました。
現段階で確定しているのは、双方の説明が食い違い、数学的正しさとは別に、着想とデータの来歴を検証する必要が生じたことです。

研究予算は「探索」と「検証」を分けて持つ

この規模のAI研究は、利用料だけを一つの費目に置くと管理できません。 予算は、仮説を広く試す探索、途中成果を統合する工程、形式化、外部専門家の再検証に分ける必要があります。
1300億出力トークンは規模を示しますが、社内モデルの原価や計算資源の単価は公開されていないため、外部API価格を掛けて費用を決めることはできません。
WIREDとAxiosは、OpenAI幹部が計算費用を数百万ドル規模と説明したと報じていますが、内訳は非開示です。

社内で似た仕組みを導入するなら、最初から1万体を動かす話にはなりません。
小さな並列探索で、単独モデルより再現率が上がるかを測り、正しい候補一件を得る計算費用を置きます。
その後に、形式検査できる領域、専門家が目視する領域、公開前に別チームが反証する領域を決めます。
探索量を増やすほど答えの候補は増えますが、検証側が細ければ、未確認の成果が積み上がるだけです。

もう一つの費用は来歴管理です。
どの資料を読ませ、どの中間結果が次のエージェントへ渡り、誰が最終判断したかを残さなければ、成果が出た後に独立性を説明できません。
研究者の未公開データを扱うサービスでは、学習利用の有無、保持期間、管理者が閲覧できる範囲を契約とログの両方で確認する必要があります。
今回の論争は、答えの性能だけでなく、研究基盤への信頼が事業価値を左右することも示しました。

見立てと監視ポイント

• 第三者による再検証 — 数学者が論文とLeanコードを動かし、公式問題との対応や隠れた仮定に具体的な反例を出すか、支持するかを追います。
• 掲載と受容の段階 — 査読付きの適格媒体へ掲載されるか、その後の議論で一般的受容が形成されるかを見ます。最低2年という時間は短縮できません。
• 研究データの来歴 — OpenAIが探索ログ、学習データの扱い、外部研究との時系列をどこまで検証可能な形で開示するかが、次の共同研究の信頼条件になります。

腹落ち確認の問い

Leanで最後まで検査できる証明が公開された後も、人間の数学者と第三者機関には何を確かめる役割が残るでしょうか。

もっと詳しく知りたい人へ

• 一次情報: OpenAIの研究発表 — 結果の範囲、約1万体の探索、計算量、外部研究への説明を確認できます
• 一次情報: 公開論文「Finite Time Blowup for Navier–Stokes」 — 定理、物理的な構成、165ページの証明全体を読めます
• 一次情報: Lean形式証明の公開リポジトリ — 形式化した定理と第三者が検査する手順を確認できます
• 制度資料: Clay Mathematics Instituteの公式規則 — 適格媒体、最低2年、一般的受容という認定条件が分かります
• 独立報道: Scientific Americanの検証記事 — 数学者の初期評価と研究上の帰属を巡る争点を追えます
• 関連する業界の見取り図: 情報・通信業業界基礎ガイド — AIを含む情報サービスの事業構造と費用の見方を確認できます