2026年9月、AIが数学の最高難度の問題に答えを出した
2026年9月8日、OpenAIが、ナビエ–ストークス方程式に関するミレニアム懸賞問題について、自社の社内モデルが生成した証明を公開しました。解析的な証明と、Lean（定理証明支援系）による形式化の両方が添えられています。
ナビエ–ストークス方程式は、流体の運動を記述する基礎方程式です。航空機の設計にも、天気予報にも、私たちが日常的に行っている流体解析にも、この方程式が使われています。その方程式について約90年間未解決だった「滑らかに始まった流れが、有限の時間で破綻することがあり得るか」という問いに、AIが答えを出した。しかも、もっともらしさが一切通用しない領域で。この出来事自体は、まちがいなく大きな節目です。
ただ、この件を追いかけるうちに、私たちが日々の解析業務で向き合っている問題と、驚くほど同じ構図が浮かび上がってきました。本稿はその話です。
見出しと、実際に証明されたことのあいだ
まず、何が証明されたのかを正確に見ておきます。
ミレニアム懸賞問題としてのナビエ–ストークス問題は、クレイ数学研究所の公式の問題文で、4つの選択肢（A）〜（D）に分けて記述されています。このうち（A）と（B）は外力を加えない場合、（C）と（D）は外力を加える場合です。
今回示されたのは、（C）と（D）にあたる結果でした。空間的にも時間的にも限られた範囲にだけ働く滑らかな外力を加えると、静止状態から出発した流れが、運動エネルギーを有限に保ったまま、有限時間で速度を無限大に発散させる。そういう解を構成した、という内容です。
一方、（A）と（B）、つまり外力を加えない場合については、未解決のまま残っています。「ナビエ–ストークス問題が解かれた」という見出しから多くの人が思い浮かべるのは、おそらくこちらの外力なしの版です。
ここで強調しておきたいのは、これは発表側の不誠実さの話ではない、ということです。OpenAI自身が発表文の中で、確立したのは（C）と（D）であると明記しており、ミレニアム賞を請求する意向はないとまで述べています。論文本文も、定理の直後に「Feffermanの問題文における選択肢（C）を確立する」と自ら範囲を限定しています。
それでも、精密に述べられた結果と、それが受け取られる姿のあいだには隙間が生まれます。結果が正しいことと、その結果が何についての結果なのかが正しく伝わることは、別の問題なのです。
「形式検証済み」が保証してくれること、してくれないこと
今回の件で技術的に最も注目すべきなのは、Leanによる形式化が添えられている点です。
形式検証とは、証明の各ステップを機械が一つずつ検査し、論理的な飛躍が一箇所もないことを確認する仕組みです。人間の査読では見落とされ得る微細な穴を、機械的に塞ぐことができます。以前の記事「AIが生成した計算は、AIに判定させてはいけない」で、AIの出力をAIに判定させる循環を断つために機械的な検査を組み込む設計について書きましたが、形式検証はその発想の、最も厳密な到達点だと言えます。
ところが、今回の件はそれと同時に、形式検証の射程の限界も示しています。
形式検証が保証するのは「書かれた命題から、結論が正しく導かれること」であって、「その命題が、あなたの解きたかった問いだったか」ではありません。
（C）と（D）を確立した証明は、形式的に完璧であり得ます。実際に機械が検査を通したのですから、そこに論理の穴は無いのでしょう。しかしそれは、（A）と（B）について何も言っていません。証明の内部をどれだけ厳密に検査しても、「証明の外側」にある問い、すなわち何を証明の対象に選んだのかという問いは、検査の対象になっていないのです。
解析の実務に置き換えると、この構図はすぐに見慣れたものになります。計算が綺麗に収束した。メッシュを細かくしても結果が動かなくなった。ベンチマーク問題とも一致した。それでも、境界条件の置き方が実機と違っていれば、その解析は正しく間違っているのです。数値的には非の打ちどころがなく、答えている問いが違う。
生成は速く、検証は遅い
もう一つ、この件が突きつけている構造があります。
OpenAIの発表によれば、証明に到達するまでに要したのは、最初のエージェントを起動してから約88時間でした。Leanによる形式化と検証には、さらに17時間。合わせて5日足らずです。
一方、数学コミュニティによる独立した検証は、発表から3週間を過ぎた本稿執筆時点でも進行中で、研究者からの批判も出ています。形式検証が済んでいてなお、こうなります。形式化された命題が、本当に意図した命題を写し取れているか。証明の構成に用いられた定式化が妥当か。そうした判断は、機械ではなく人間が担う部分として残るからです。
つまり、生成の側のコストは劇的に下がったが、検証の側のコストは同じようには下がっていない。この非対称性は失敗ではなく、これからの標準的な姿だと考えたほうがよさそうです。そして非対称であるということは、検証が律速段階になるということでもあります。
実務の解析で、同じ構図がどう現れるか
私たちが開発している解析パイプラインでも、検証は二つの層に分かれます。
**第1層は「答えが正しいか」**です。計算式と予測値のあいだに自己矛盾がないか。解像度を変えても結果が安定するか。理論的な厳密解や、業界規格が定める式と突き合わせて一致するか。この層は機械的に検査できます。判定をAIに委ねる必要はなく、決められた手順どおりにしか動かないプログラムで十分です。
**第2層は「正しい問いを解いたか」**です。その境界条件は実機の状況を写しているか。選んだ材料モデルは、想定している変形の範囲で妥当か。そしてその解析が答えている問いは、お客様が本当に判断したい問いと一致しているか。この層は、今のところ機械化できていません。
そして、実務で事故になるのは、たいてい第2層です。
つい先日、私たち自身がまさにこの層で足をすくわれかけました。流体解析の検証基準として、ある古典的な理論解を採用しようとしたときのことです。その理論解の正確な係数を、一次資料まで遡って確認し、自分たちの計算の条件に合わせて変換する作業まで終えていました。式そのものは正しい。変換も正しい。ところがその後で、その理論が前提としている流れの状態と、私たちが計算しようとしていた形状とが噛み合っていないことに気づきました。第1層の意味では何も間違っていないのに、突き合わせ自体が成立しない状況だったのです。結局、検証の土俵に載せられる形状のほうを設計し直しました。
式を確認して終わりにせず、その式が要求している前提が自分たちのケースに本当に当てはまるかを、実装前にもう一段確かめる。この一手間は、AIによって計算の生成が速くなるほど、相対的に重みを増していきます。
それでも、これは大きな出来事である
ここまで慎重な読み方を続けてきましたが、最後に逆側のことも書いておきます。
今回の成果を「見出しほどではなかった」と切り捨てるのは、正確ではありません。外力を加えた場合とはいえ、ナビエ–ストークス方程式の解が有限時間で破綻し得ることを厳密に構成してみせたのは、それ自体が流体力学の難問に対する本物の前進です。加えて、ほぼ同時期に、別の研究者らが隣接する問題（外力を加えたオイラー方程式）について独立に結果を得ており、双方が先行性を認め合う形で公表されています。どちらの結果も、AIを研究の中核に据えた取り組みから出てきました。
そして何より、もっともらしい答えが一切通用しない領域に、AIが上がってきたという事実があります。数学の証明は、それらしく見えるかどうかでは評価されません。通るか、通らないか、それだけです。その土俵に立ったこと自体は、結果の最終的な評価を待たずとも動きません。
だからこそ、検証のあり方が問われます。生成する力が上がるほど、「それは何についての答えなのか」を確かめる力が、相対的に希少になっていくからです。
ご相談の流れ
「AIを使った解析結果を、どう受け取ればいいのか」「その解析が、本当に自分たちの知りたいことに答えているのか分からない」。そうした場面でこそ、第三者の目が効きます。数理物理研究所では、AIを積極的に活用しながらも、その出力を機械的に検証する仕組みと、問いの立て方そのものを点検する視点の両方を組み込んだ形でのご支援を承っております。まずはお気軽にご相談ください。