作成日: 2026-09-09

参考文献

この記事で分かること

2026年9月、OpenAIが「3次元のナビエ-ストークス方程式は、外からの力を加えると有限の時間で破綻する」ということを、AIエージェントの大群を使って証明したと発表した。数学の未解決問題の中でも特に有名な「ミレニアム懸賞問題」の一つに関わる話で、報道によっては「AIが100万ドルの問題を解いた」というような書かれ方もされている。

結論から言うと、それは正確ではない。ただし、正確に理解すると、むしろ元の話よりも面白い。この記事では、

  1. そもそも何が証明されたのか
  2. なぜ「懸賞問題を解いた」は言い過ぎなのか
  3. 証明の中身(どうやって方程式を「壊す」のか)
  4. 証明を作ったAIエージェントたちの動き方(ここが一番ユニーク)
  5. 「証明された」の正確な意味と、誰も見ていないわけではない優先権論争

の順に説明する。

1. ナビエ-ストークス方程式とは何か、なぜ有名なのか

ナビエ-ストークス方程式は、水や空気のような流体がどう動くかを記述する方程式で、天気予報から飛行機の設計まで、あらゆる流体シミュレーションの土台になっている。

この方程式には長年未解決の疑問がある。「なめらかな(角がなく、値が無限大に飛ばない)初期状態から出発して、方程式に従ってずっと時間発展させ続けたとき、途中で値が無限大に発散してしまう(=方程式が『壊れる』)ことは起こり得るのか、それとも永遠になめらかなままなのか」という問いだ。

クレイ数学研究所はこれを「ミレニアム懸賞問題」の一つに指定し、100万ドルの懸賞をかけている。ただし、この懸賞問題にはいくつかの選択肢があり、そのうちの一つを証明すれば懸賞が成立する、という構造になっている。今回のAIによる証明は、この選択肢のうち「外力を加えた場合に破綻する例を作れ」という部分に対応するもので、「外力なしでも必ずいつかは壊れる」あるいは「外力なしなら絶対に壊れない」という、懸賞問題の中核をなす主張には答えていない。

つまり今回の成果は、懸賞問題そのものの解決ではなく、懸賞問題に隣接する、しかし依然として重要な問いへの答えである。

クレイ研究所の懸賞問題、4つの選択肢

クレイ数学研究所の公式問題文は、以下の4つのうち、いずれか1つを証明すれば懸賞が成立する、という形になっている(これらは数学者Charles Feffermanが作成した公式ステートメントによる)。

選択肢舞台となる空間外力証明すべき内容
(A)無限に広がる空間(R³)なしどんな滑らかな初期状態から出発しても、解は永遠に滑らかであり続ける
(B)周期的な空間(トーラスT³、宇宙の果てまで行くとまた元の場所に戻る空間)なしどんな滑らかな初期状態から出発しても、解は永遠に滑らかであり続ける
(C)無限に広がる空間(R³)あり解が有限時間で破綻する(滑らかでなくなる)、滑らかな初期状態と外力の組が存在する
(D)周期的な空間(トーラスT³)あり解が有限時間で破綻する(滑らかでなくなる)、滑らかな初期状態と外力の組が存在する

(A)(B)は「外力なしで、方程式は永遠に破綻しないことを証明せよ」という方向、(C)(D)は「外力ありなら、破綻する具体例を作れ」という方向で、証明すべき内容が正反対であることに注意してほしい。

今回のOpenAIの結果は、このうち (D)(周期空間・外力あり・破綻の具体例)に対応する。天気予報や航空機設計が前提としているのは外力がゼロか、あってもごく自然なものに限られる状況であり、それに一番近いのは(A)(B)、つまり「外力なしでも本当に永遠に滑らかなままなのか」という問いだ。ここが依然として未解決のまま残っている。

2. 何が証明されたのか(正確な主張)

今回証明されたのはこういう主張だ。

どんなに小さい粘性(流体のねばり具合)を選んでも、ある特殊な「外から加える力」と、静止した状態から出発する滑らかな流れが存在して、その流れは運動エネルギーを有限に保ったまま、決まった時刻(t=1としておく)に向かって速度が無限大に発散していく。

これは、無限に広がる空間(R³)でも、有限の箱を繰り返し並べたような空間(トーラスと呼ばれる、宇宙の果てまで行くとまた元の場所に戻ってくるような空間)でも、両方で成り立つことが示された。

重要なのは「外力あり」という条件だ。外力を自由に設計してよいなら、方程式にエネルギーを送り込む蛇口を自分で用意できることになる。これは「外力なし」の場合よりも明らかに易しい設定であり、専門家の間でも「外力ありの破綻例は、外力なしの場合よりずっと構成しやすいはずだ」という予測は以前からあった。今回の成果は、その予測されていた方向を実際に厳密な証明の形にまで仕上げた、というのが正確な位置づけになる。

3. どうやって「壊す」のか — 渦を煙突のように縮める

数式を使わずに、証明の核心にあるアイデアを説明する。

想像してほしいのは、フィギュアスケーターが両腕を体に引き寄せると回転が速くなる、あの現象だ。体の質量(回転の勢い)が変わらないまま、腕が縮んで体の中心に近づくと、回転角速度は上がる。これは「角運動量保存」と呼ばれる性質のミニチュア版で、流体の渦にも似た効果が働く。

証明で作られる「破綻する解」は、円柱のような形をした渦を用意し、その渦を時間とともに原点に向かって細く絞り込んでいく設計になっている。ポイントは、渦の「半径方向の太さ」と「軸方向(円柱の長さ方向)の長さ」を、わざと違う速さで縮めることだ。半径のほうを軸の長さより速く縮めていく。すると、渦の中身(体積)はどんどんゼロに近づきながら、細長い糸のような形になっていく。

流体は基本的に「潰れない」性質(非圧縮性)を持っているので、半径方向にどんどん押し縮められた分は、行き場をなくして軸方向に押し出される。この押し出しと、角運動量保存的な効果が組み合わさることで、渦の回転はどんどん速くなっていき、時刻がt=1に近づくにつれて速度が発散する — これが破綻の仕組みだ。

この設計には、もう一つ興味深い非対称性がある。渦の「回転方向の乱れやすさ」を表す指標(角方向のレイノルズ数、と呼ばれる)は、時刻が進むにつれて無限大に発散していく一方で、「半径方向の広がり方の乱れやすさ」を表す指標は有限のまま抑えられている。つまり、回転方向は制御を失って暴れていくのに、半径方向の広がりは粘性(流体のねばり)がきちんと押さえ込み続ける。この片方だけ暴れて片方は抑えが効く、という非対称なバランスこそが、証明全体を成立させる鍵になっている。

なぜ外力が必要なのか

ただし、この「絞り込まれる渦」を単独で置いただけでは、うまくいかない。渦の外側には、遠くに行くほど指数関数的に静かになっていく穏やかな流れがあるはずだが、渦とその外側の穏やかな流れの「つなぎ目」で、運動量の帳尻が合わなくなってしまう(数式上、残差が発散してしまう)問題が生じる。

これを解決するために、証明では、空間的にも時間的にも局所的に存在するが、方位角方向(渦の周りをぐるっと回る方向)には全周にわたって作用する「振動するパルス」を2種類、追加の力として重ねて加える。このパルスは、背景にある回転のずれ(場所によって回転の速さが違う効果、回転シア)からエネルギーを吸い上げて指数関数的に増幅していき、非線形の相互作用を通じて、渦と外側のつなぎ目のつじつまを合わせるのに必要な力を供給する。

同時に、このパルスの径方向の波長(細かさ)は時間とともにどんどん短く設計されており、最終的には粘性による減衰の効果が増幅の効果を上回るように精密に制御されている。これによって、特異点に到達する瞬間まで、加えている力そのものは終始なめらかで、かつ有限の範囲に収まったまま(コンパクトサポート)であり続けるように仕組まれている。

4. AIエージェントたちはどう動いたのか(この記事の一番の見どころ)

証明そのものと同じくらい興味深いのが、これがどうやって作られたかというプロセスだ。

OpenAIの発表によれば、最大で約1万体のAIエージェントが並行して稼働し、9月1日に探索を開始、9月5日には証明にたどり着いた。所要時間は88時間。この間、エージェント同士でやり取りされたメッセージは270万通、生成された出力トークンの総量は約1300億に達したという。個々のエージェント同士の議論をとりまとめ、グループ間の知見を統合する役回りは、コード生成AIであるCodexが担った。

この探索プロセスで特に面白いのは、次の2点だ。

1つ目は、証明と反証を最初から同時に狙わせていたこと。 あるグループのエージェントには「この方程式は常になめらかなままである(=壊れない)ことを証明せよ」という課題を、別のグループには「破綻する例を作れ(=壊れることを証明せよ)」という、正反対の課題を同時に与えていた。つまり、最初から「答えがどちらに転ぶか分からない」状態で、両方の可能性を本気で追わせていたことになる。これは、片方の結論に最初から決め打ちして探索資源を注ぎ込むよりも、真実がどちらであっても取りこぼさない設計だと言える。

2つ目は、本題とは違うところから生まれた偶然の副産物が、方針転換の決め手になったこと。 全体のうちの比較的小さなサブグループ(約100体)が、本題であるナビエ-ストークス方程式そのものではなく、粘性を取り除いたより単純な「オイラー方程式」における特異点の問題に、約50時間かけて取り組んでいた。ところが、このサブグループが予想外のブレークスルーを達成し、その知見がメインの探索グループにフィードバックされたことで、全体の方針が大きく前進した。

最初から狙って設計された成果ではなく、脇道で得られた発見が本流に合流して事態を動かした、という展開になっている点は、人間の研究チームでもしばしば起こることと重なる部分があり興味深い。

そして最後の17時間は、それまでとは別の、まだ一般公開されていない新しいモデルが、できあがった証明をLean(数学的な証明を1ステップずつ機械的にチェックできるプログラミング言語のようなもの)で形式検証する作業に充てられた。

5. 「証明された」の正確な意味 — 何がまだ済んでいないか

そもそもLeanとは何か

Leanは、数学の証明を「1行ずつコンピュータが検証できる形」に書き下すためのプログラミング言語(および、そのためのソフトウェア環境)だ。普通、数学の証明は人間が読んで「論理の飛躍がないか」をチェックするが、Leanで書かれた証明は、公理(証明の前提として最初から正しいと認められているルール)からの一つひとつの推論ステップを、コンピュータが機械的に検証してくれる。

たとえるなら、将棋や囲碁の「棋譜が本当にルール通りの手順で進んでいるか」を、コンピュータに1手ずつチェックさせるようなものだ。手順(論理展開)がルール(公理系)に反していないかは機械が確実に保証してくれるが、その手順が「良い戦略だったか」「本当に勝ちに繋がる意味のある手だったか」は、また別の話になる。数学の証明で言えば、論理的な正しさ(Leanが保証する部分)と、その証明が主張しようとしている中身が正しく言い表せているか(人間が確認すべき部分)は、別々にチェックする必要がある、ということだ。

近年、Google DeepMindやOpenAIなど大手AI企業の数学系の取り組みでもLeanが標準的に使われており、AIが生成した証明の信頼性を担保する手段として定着しつつある。

証明はこのLeanによって形式検証されており、そのコードはGitHub上で公開されている(openai/NavierStokesAndEuler)。これは、証明の一つひとつの論理ステップが、確かに正しい推論になっているということを機械的に保証するものであり、非常に強い裏付けではある。

ただし、これで「すべてが完全に確定した」わけではないことには注意が必要だ。少なくとも次の2点は、形式検証とは別問題として残っている。

  • 形式化された命題文(コンピュータが検証した「文」そのもの)が、もともと意図していた数学的な主張を正しく捉えているかどうかは、人間の目によるチェックが必要な部分である。
  • 証明が持つ数学的な意義や、他の設定への一般化可能性については、専門家コミュニティによる吟味がこれから行われる段階にある。

2026年9月時点で、クレイ数学研究所による正式な査読や受理は行われていない。したがって、現時点では「専門家コミュニティによる検証待ちの、有力な証明」という位置づけが正確であり、「懸賞問題が解決した」という報じ方は誤りである。

Palasekによる技術的な指摘

プリンストン大学の数学者スタン・パラセック(Stan Palasek)は、今回の手法を「外力なし」の場合にそのまま拡張しようとすると、技術的な障害にぶつかることを指摘している。具体的には、粘性による散逸(エネルギーが失われていく効果)が、遠く離れた周波数(スケール)同士が相互作用しながら積み上がって成長していくメカニズムを上回ってしまう、というものだ。これは簡略化されたモデル(シェルモデルと呼ばれる、本来の方程式を扱いやすく単純化したモデル)を使った議論であり、今回発表された「外力あり」の結果そのものを否定するものではない。

Terence Taoもこの指摘を歓迎しており、より単純なモデルを使ってこの相互作用の仕組みをはっきりさせる追加の研究を提案している。要するに、「外力なし」の場合(=懸賞問題の中核)は、今回の成果をもってしても依然として手強い問題として残っている、ということだ。

6. 優先権をめぐる論争

今回の発表をめぐっては、優先権(誰が先にどこまでやったか)についての論争も起きている。

NYUの数学者トリスタン・バックマスター(Tristan Buckmaster)とAnthropicのレベント・アルプージ(Levent Alpöge)は、オイラー方程式・多孔質媒体方程式・ブシネスク方程式について、今回と類似した「自己相似的な特異点」の構成を、Leanによる形式検証込みで、独立に先行して発表していた。

Fortune誌の報道によれば、9月6日の電話で、OpenAI側の人物(Bubeck)から、バックマスターに対して「アルプージを著者から外せば、あなたの受賞主張を認める」という趣旨の提案があったと、バックマスター本人が主張している。バックマスターはこれを拒否したところ、「キャリアを台無しにするつもりか」という趣旨の発言をされたとも訴えている。

これに対しOpenAI側は、アルプージを外すことを求めた、という意図自体は否定している一方で、発言の表現自体については謝罪し撤回したとしている。アルプージ本人はこの通話をたまたま耳にする形で聞いており、「除外がすでに既定路線であるかのように受け取った」と述べている。これに対しBubeckは「その議論はまだ確定していなかった」と反論しており、双方の主張は食い違ったままになっている。

Terence Taoは、両者の業績をいずれも高く評価する立場を取りつつ、「ミレニアム懸賞問題全体が解決した」という一般的な受け止め方は誤りであると訂正している。さらにTaoは、AI企業が未解決問題を性急に”採掘”するような競争が起きることで、失敗した試み(袋小路)が非公開のまま埋もれてしまい、数学研究コミュニティ全体が積み重ねてきた「知見を共有する文化」が損なわれることへの懸念も表明している。

まとめ — 率直にすごい点と、まだ終わっていない点

率直にすごいと思う点

  • 1万体規模のAIエージェントが88時間で、専門家でも一朝一夕には到達できない水準の構成的証明を作り上げ、形式検証まで終えたという事実そのもの。
  • 証明と反証を同時に狙わせる設計や、脇道の発見(オイラー方程式でのブレークスルー)が本流にフィードバックされて方針転換を生んだ経緯は、AIによる数学探索の進め方として示唆に富む。
  • 渦を非対称な速さで絞り込むという構成のアイデア自体は、たとえAIが発見したものであっても、数学的な独創性として評価に値する。

まだ解決していない点

  • 今回証明されたのは「外力あり」の破綻であり、クレイ数学研究所の懸賞問題の中核をなす「外力なし」の場合(壊れるのか、永遠になめらかなままなのか)には、依然として答えていない。Palasekの指摘が示すように、外力なしの拡張には技術的な障害がある。
  • 形式検証は済んでいるが、命題文が意図を正しく捉えているかの人間によるチェックと、専門家コミュニティによる意義の吟味は、まだこれからの段階にある。クレイ数学研究所による正式な査読・受理も行われていない。
  • 優先権をめぐる論争は決着しておらず、双方の言い分が食い違ったまま残っている。

以上を踏まえると、今回の一件は「懸賞問題が解けた」という単純な話ではなく、「AIによる数学探索が、専門家の予測していた方向で、専門家レベルの構成的証明を実際に作れることを示した」という、それ自体として評価に値する、しかし限定的な成果として理解するのが正確だろう。