2026年9月1日、OpenAIは約90年間未解決だったナビエ–ストークス方程式の問題に、大量のAIエージェントを投入しました。
エージェントが解答に到達したのは9月5日。最初のエージェントを動かしてから約88時間後です。その後、別のAIモデルを使って17時間かけて証明をLeanへ形式化し、9月6日に検証を完了。9月8日、OpenAIは論文とLeanによる形式証明を公開しました。
動いたAIエージェントは約1万体。
ナビエ–ストークス問題だけで270万件のメッセージをやり取りし、約1300億の出力トークンを使っています。OpenAIが同時期に試した数学問題全体では490万メッセージ、約3000億トークンに達しました。
OpenAIは、これによってミレニアム懸賞問題を解決したとしています。
ただし、2026年9月時点でClay Mathematics Institute（CMI）はナビエ–ストークス問題を「Active」として掲載しています。CMIは9月11日、声明で今回の発表について「apparently been settled（解決されたようだ）」と表現し、既定の手続きに従って成果とクレジットを評価するとしています。
CMIの規則では、候補となる解答が所定の媒体に掲載されてから少なくとも2年が経過し、世界の数学界で広く受け入れられることなどが審査の前提です。OpenAI自身も100万ドルの賞金を請求しない方針を表明しています。
約1万体のAIは何を証明したのか
ナビエ–ストークス方程式は、水や空気などの流体がどのように動くのかを記述する方程式です。
飛行機の周囲を流れる空気、海流、配管を流れる水など、さまざまな流体現象の数学的な基礎として使われています。
方程式自体は19世紀から知られていますが、3次元の場合に、滑らかな初期状態から始めた流体が、その後もずっと滑らかであり続けるのかは分かっていませんでした。
問題になるのが「特異点」です。
流体の速度などが有限のまま正常に推移するのではなく、ある有限の時間で数学的に無限大へ発散するような状態を考えます。
Clay Mathematics Instituteが定めた問題では、大きく言えば「常に滑らかな解が存在する」と証明する方法と、「条件を満たしていても解が破綻する例が存在する」と証明する方法のどちらでも決着できます。
OpenAIが提示したのは後者です。
滑らかな外力を受ける流体について、エネルギーは有限に保たれているにもかかわらず、有限時間で特異点が生じる例を構成しました。OpenAIは、公式問題記述のStatement CとDを満たすと説明しています。
証明はLeanでも形式化されています。
Leanは、証明の各ステップが論理規則に従っているかをコンピューターで検証できる定理証明支援系です。人間が長大な証明を一行ずつ確認する場合とは異なり、形式化された証明について論理的な抜けを機械的に検査できます。
それでも、「Leanで通ったから数学界の審査が終わった」という話にはなりません。
Leanで確認できるのは、形式化された命題から結論までの論理です。その形式化が元のミレニアム懸賞問題を正確に表しているか、証明が既存研究の中でどのような数学的価値を持つのかは、人間の数学者による検討が残ります。
「証明の希少性」がなくなる
数学研究を大まかに分けると、問いを立て、使えそうなアイデアを探し、証明を組み立て、その証明から何が分かるのかを理解するという過程があります。
AIが急速に入り込んでいるのが、アイデアの探索と証明の生成です。
数学者Terence Taoは、AIによって数学が「proof scarcity（証明の希少性）」から「proof abundance（証明が豊富に存在する状態）」へ向かう可能性を指摘しています。
AIが正しい証明を大量に作れるようになったとき、次に問題になるのは、人間がその結果をどう理解するかです。AIが数学を解きすぎる？テレンス・タオが考える「理解」の問題では、テレンス・タオ氏が論じる「proof abundance（証明の豊富さ）」と「proof indigestion（証明の消化不良）」を中心に、AI時代に人間の「理解」がなぜ希少になるのかを詳しく整理しています。
今回のナビエ–ストークス問題では、その言葉をかなり具体的に想像できます。
約1万体のエージェントを同時に動かし、それぞれに異なる方向を探索させる。失敗する経路が大量にあっても構わない。有望なアイデアだけを集め、次の探索へ渡していく。
人間の数学者が一つの証明へ長い時間を費やしていた状況と、探索できる候補の数がまるで違います。
証明を大量に生成できるようになると、別の作業に時間がかかります。
大量に出てきた結果のうち、どれに価値があるのか。似た定理との関係はどうなっているのか。その証明から新しい数学的な考え方を取り出せるのか。
証明そのものの供給量が増えても、それを読む人間の時間は増えません。
形式証明によって「正しいか」を確認できたとしても、「なぜこの方法で解けたのか」「他の問題へ使える考え方は何か」という理解まで自動的についてくるわけではありません。
Scienceは今回の出来事を、数学界に「existential crisis（実存的危機）」を引き起こしたと表現しました。
数学者という職業が直ちになくなるという話よりも、数学者が時間を使ってきた活動のどこに価値を置くのかが揺さぶられている、と読む方が実態に近そうです。
AIに未公開研究を相談しても大丈夫なのか
今回の発表では、研究成果の優先権とAIサービスへ入力したデータの扱いをめぐって、OpenAIと研究者の間にかなり具体的な対立も起きました。
ニューヨーク大学のTristan BuckmasterとAnthropicのLevent Alpögeは、OpenAIとは別にEuler方程式に関する研究を進めていました。
Euler方程式はNavier–Stokes方程式と近い関係にあります。ただし、BuckmasterとAlpögeが解いたのは外力を加えたforced Eulerの問題で、OpenAIが得た外力なしのEuler方程式やNavier–Stokesの結果とは同じ問題ではありません。OpenAIも両者のforced Eulerにおける優先権を認めています。
OpenAIによると、9月1日に「2つのミレニアム懸賞問題が解かれたらしい」という噂を聞き、新しい内部モデルを使った探索を開始しました。その噂が後になってBuckmasterとAlpögeの研究に関係していたと分かった、と説明しています。
Buckmaster側の説明は、これよりかなり険しいものです。
BuckmasterはOpenAIの発表に先立って自ら経緯を公開しました。彼は、自分たちの研究の進展に関する情報がOpenAIへ伝わった後にOpenAI側の探索が始まり、非常に大きな計算資源が投入されたと説明しています。
さらにBuckmasterは、研究の過程でCodexを継続的に利用し、プロジェクトの草稿を入力していたため、それらのデータがOpenAIのモデルへ何らかの形で影響した可能性について質問しました。
Buckmasterの説明では、モデルがユーザーデータを直接参照したかという質問には否定的な回答を受けたものの、訓練への利用について改めて尋ねた際には回答を得られなかったとしています。
OpenAIは9月10日に公式ページを更新し、発表前2カ月間のBuckmasterのCodexプロンプトを調査した結果、今回利用した内部モデルには訓練を含めて影響していなかったと発表しました。
両者の対立はデータ利用だけではありません。
Buckmasterによれば、OpenAI側から二つの提案を受けました。
一つは、BuckmasterとAlpögeがEulerの成果を先に公開し、翌日にOpenAIがNavier–Stokesの結果を公開するという案です。
もう一つは、Eulerの成果を公開した後、Buckmaster自身がOpenAIのNavier–Stokes結果を書き直して論文にするという案でした。Buckmasterはこの提案について、OpenAIのSébastien BubeckがAlpögeを著者から外すことを二度求め、Anthropic勤務であることを理由として挙げたと説明しています。Buckmasterは両案を拒否しました。
Bubeck側の説明は異なります。
ABC Newsによると、BubeckはAlpöge自身の研究から名前を外すよう求めたわけではなく、OpenAIの証明を書き直す論文にAnthropic社員を著者として入れるのは不適切だと考えた、と説明しています。
さらにBuckmasterは、OpenAIが提案した形で結果を発表するなら経緯を公表すると伝えた際、Bubeckから「Why would you ruin your career?」と返され、その後「If you don’t want me to be nice, then I don’t have to be nice」と言われたとしています。
Bubeckは後に、この発言について言葉の選び方が極めて悪かったとして謝罪しました。一方で、Buckmasterを脅す意図ではなく、根拠のない非難によって研究者自身の評判を傷つけることを心配していたという趣旨の説明をしています。
Buckmaster自身も、自分たちのデータが実際に使われたことを証明できるわけではない、と明言しています。New York Timesの取材でも、証拠はないとしながら、OpenAIの証明のアプローチと出来事の時系列から強い疑念を持っていると述べています。
そのため、「OpenAIが研究を盗んだ」と事実として書ける状況ではありません。
一方で、「研究者自身がどのような疑念を持ち、OpenAIとの間でどのようなやり取りがあったのか」まで削ってしまうと、この論争の実態も見えなくなります。
研究者がAIへ未公開のアイデアや草稿を入力する状況では、実際にデータが利用されたかどうかだけでなく、運営企業にどこまで研究内容を知られるのかという信頼の問題が生まれます。
研究支援AIが高性能になるほど、そこへ価値の高い未公開情報を渡したくなる。その一方で、AIサービスの提供企業自身が同じ研究領域で競争者になる可能性も出てきました。
約1万体のAIを「研究組織」として動かした
OpenAIの発表で見逃せないのが、モデルそのものより運用方法です。
約1万体のAIに同じ質問を投げて、多数決を取ったわけではありません。
OpenAIはエージェントを複数のグループへ分け、それぞれに異なる方法を探索させました。グループ内のエージェントは互いに通信でき、途中で有望な知見が出るとCodexを使って複数グループの結果を統合し、その情報を次の探索へ投入しています。
ナビエ–ストークスへ到達する前には、約100体のエージェントを約50時間動かし、外力のないEuler方程式についてregularityを反証する結果を得ました。
OpenAIはその結果を見て、ナビエ–ストークスが最も有望だと判断。他のミレニアム問題からエージェントを移し、Eulerで得た結果も与えて集中探索させています。
探索の途中で、さらに訓練が進んだ内部モデルが利用可能になると、動いているエージェントを新モデルへ更新しました。
研究テーマを複数走らせ、途中の成果を評価し、有望なテーマへ人員ならぬ計算資源を再配置し、チーム間で情報を共有する。
運用だけを見ると、研究室や企業の研究開発組織にかなり近い形です。
AI研究というと、研究者が一つのモデルへ相談し、その回答を手がかりに研究を進める姿を想像しがちです。今回OpenAIが示したのは、研究者の下に巨大なAI研究チームを置く形でした。
人間の天才とAIが一対一で能力を競う構図では捉えにくくなっています。
研究者一人が、自分では到底試せない数の仮説や証明方針を並行して走らせ、その中から有望な結果だけを拾えるからです。
計算資源を大量に持つ組織ほど、この方法を大規模化できます。
数学の研究競争には、研究者の能力だけでなく「何体のAIエージェントを、どれだけ長く動かせるか」という条件まで入り始めています。
証明が増えすぎた世界で数学者は何をするのか
AIが証明を作れるようになったからといって、人間が証明を作らなくなると決まったわけではありません。
今回の証明も、何もない場所から突然現れたものではありませんでした。
Diego CórdobaやLuis Martínez-Zoroa、Fan ZhengらによるEuler方程式やNavier–Stokes方程式周辺の研究があり、BuckmasterとAlpögeの成果もその流れを引き継いでいます。OpenAIの探索も、こうした数学研究の蓄積の上で行われています。
一方、証明を生成するコストが大幅に下がれば、数学者が使う時間の配分は変わる可能性があります。
どの問題をAIに解かせるのかを選ぶこと。生成された証明の価値を評価すること。別々に得られた結果の関係を見つけること。そして、証明がなぜ成立するのかを人間が理解できる形へ整理することです。
Clay Mathematics Instituteは、ナビエ–ストークス問題を紹介するページで、証明を求める理由について「証明は確実性だけでなく、理解も与える」と説明しています。
AIが確実性へ到達する速度を大きく上げたとき、その後に残る「理解」を誰が作るのか。
今回の発表が数学者へ突きつけている問いの一つです。
数学は、命題と証明を形式化できれば、コンピューターによる厳密な検証と相性のいい分野です。実験装置を動かしたり、自然界から新しいデータを取得したりする必要がある科学分野とは条件が違います。
そのため、数学で起きていることをそのまま物理学、生物学、医学へ当てはめることはできません。
一方で、数千、数万のAIエージェントを役割分担させ、互いの成果を共有しながら研究させる方法自体は数学に限定されません。
今回登場したのは、難問を解くAIだけではなく、大量のAIをひとつの研究組織として動かす研究方法でもありました。
FAQ
OpenAIはナビエ–ストークス問題を正式に解決したのですか？
OpenAIは、ミレニアム懸賞問題の条件を満たす証明を得たと発表し、論文とLeanによる形式証明を公開しています。
ただしClay Mathematics Instituteでは、2026年9月時点でもナビエ–ストークス問題はActiveとして掲載されています。CMIは9月11日の声明で今回の発表を「apparently been settled」と表現していますが、正式な賞の審査には既定の手続きがあります。
Leanで検証されているなら、証明は正しいと考えてよいのですか？
Leanによる形式検証は、形式化された命題から結論までの論理が正しいことを非常に強く保証します。
一方で、その形式化された命題が元のミレニアム懸賞問題を正確に表現しているか、証明が既存研究の中でどのような数学的価値を持つのかについては、人間の数学者による確認と理解が必要です。
参考・参照元
OpenAI「On the Navier–Stokes Millennium Prize Problem」
https://openai.com/index/navier-stokes-solution/
Clay Mathematics Institute「Navier-Stokes Announcement」
https://www.claymath.org/news/navier-stokes-announcement/
Clay Mathematics Institute「Navier-Stokes Equation」
https://www.claymath.org/millennium/navier-stokes-equation/
TechCrunch「OpenAI fought dirty on career-making math problem, says NYU mathematician」
https://techcrunch.com/2026/09/08/openai-fought-dirty-on-career-making-math-problem-says-nyu-mathematician/
ABC News「Controversy erupts as OpenAI claims solution to Navier Stokes maths problem」
https://www.abc.net.au/news/2026-09-10/openai-navier-stokes-millennium-problem-claims/107132242
New York Times「An N.Y.U. Mathematician Clashed With OpenAI Over a $1 Million Proof」
https://www.nytimes.com/2026/09/10/science/tristan-buckmaster-openai-math-navier-stokes.html
Science「OpenAI breakthrough triggers ‘existential crisis’ in math」
https://www.science.org/content/article/openai-breakthrough-triggers-existential-crisis-math
