9月9日、RuntimeWire.comが「OpenAI says 10,000 AI agents solved Navier-Stokes in 88 hours」と題した記事を公開した。ミレニアム問題のひとつ「ナビエ・ストークス方程式の存在・滑らかさ問題」は100年以上未解決のままだった。OpenAIはそれを約1万体のAIエージェントの協調稼働で88時間以内に証明したと主張しており、もし検証を経て認められれば数学史上最大級の出来事となる。だが査読プロセスはいまだ始まったばかりで、数学コミュニティの評価は今後数年かけて下される。
1万エージェント、88時間、約3000億トークン
OpenAIは9月9日（米国時間）、未公開モデルと約1万体のAIエージェントを使い、クレイ数学研究所が指定するミレニアム問題のひとつ「ナビエ・ストークス方程式の存在・滑らかさ問題」に対する解を得たと発表した。X上のスレッドと研究発表ページで公開された。
ナビエ・ストークス方程式は空気や水といった流体の運動を記述する偏微分方程式で、ミレニアム問題はこの方程式の解が三次元空間において常に滑らかに存在し続けるか、あるいは有限時間で速度が発散する「特異点（シンギュラリティ）」が発生しうるかを問うている。100年以上未解決の問題だ。
OpenAIが採った立場は「特異点が発生しうる」という方向だ。速度ゼロから始まり滑らかな外力を加えた三次元非圧縮性流体が、有限時間で速度が無限大に発散する状況を構成できると論じている。渦が縮小しながら軸方向に流体が引き伸ばされ、速度が発散する領域は徐々に小さくなるため、全体の運動エネルギーは有界に保たれるという構造だ。
公開されたもの、されていないもの
OpenAIは以下の資料を公開した：
- 165ページの解析的証明
- **Lean 4による形式化コード**（独立した検証が可能）
Lean 4は定理証明支援系（proof assistant）と呼ばれるシステムで、数学的命題を機械検証可能なコードとして記述できる。人間が書いた証明とは異なり、Lean 4のコードはコンパイラが論理的整合性を逐一チェックするため、「証明の見落とし」を原理的に排除しやすい。近年はTerence Taoらトップ数学者も採用しており、数学のフォーマル化において事実上の標準ツールとなりつつある。形式化コードが公開されていることで、外部の研究者が定義と定理の整合性を独自に確認できる点は、今回の発表における数少ない透明性の担保といえる。
一方で公開されていないものも多い。使用されたモデルの名称・ベンチマーク結果・エージェントのオーケストレーション詳細・コスト内訳は非公開だ。OpenAIはこのモデルを「GPT-6 Astraよりも大幅に高性能」と述べるにとどめている。
計算規模の実態
エージェント数だけが大きいのではなく、生成されたデータ量も桁違いだ。
- ナビエ・ストークス問題だけで270万件のメッセージ、約1300億トークンを出力
- 複数問題への挑戦全体では490万件のメッセージ、約3000億トークン
- 計算費用はOpenAI幹部がプレス向けコールで「数百万ドル規模」と述べた（Axiosによる報道）
作業の流れとしては、8月28日にモデルの訓練を開始。9月1日に「ミレニアム問題が解かれたらしい」という噂を受けて残りの問題にエージェントグループを展開。初期の約100体のエージェントグループが50時間でオイラー方程式（粘性のない流体モデル）の有限時間特異点を発見し、その後リソースをナビエ・ストークスに集中。9月5日に約1万体のエージェントが結果に到達。その後、GPT-6 Astraが17時間かけてLean形式化と検証を完了した。
数学コミュニティの検証はこれから
クレイ数学研究所は依然としてナビエ・ストークス問題を未解決と分類している。クレイのルールでは、解答候補が認められるには査読付き雑誌への掲載、2年以上の公開期間、数学コミュニティ全体での受け入れが必要で、OpenAI自身も100万ドルの賞金を申請しないと述べている。
また、発表の背景に別の研究者との確執もある。OpenAIが「噂」のきっかけとしたのは、NYU数学教授のTristan BuckmasterとAnthropicの研究者Levent Alpogeによるオイラー方程式の研究だった。Buckmasterは、OpenAIが自分たちの非公開研究を無断で利用したのではないかと疑問を呈した。具体的には、両者がOpenAI製品（ChatGPTなど）を通じて研究上のやり取りや試算を行っていた可能性があり、その会話データがモデルの改善に使われた結果として、エージェントが類似のアプローチに到達したのではないかという懸念だ。OpenAIは「研究者もエージェントもその研究を事前に参照していない」と反論しつつ、「モデルの改善に匿名化されたプロダクトデータが関与した可能性は排除できない」と認めた。
Lean形式化されたコードが公開されたことで数学者が検証できる具体的な材料は揃った。ただし形式化コードの定義がクレイ問題を正確に捉えているか、解析的証明が形式化を裏付けているか、という検証はほとんど始まっていない。この問題が本当に解かれたかどうかは、88時間の生成作業ではなく、その後の数年単位の査読によって決まる。
詳細はOpenAI says 10,000 AI agents solved Navier-Stokes in 88 hoursを参照していただきたい。
