ナビエ–ストークスとLeanによる証明——強制項つき特異点と、研究所の不透明さ

2026年9月8日、OpenAIは、一般には配布していない社内モデルが、3次元非圧縮ナビエ–ストークス方程式について有限時間での爆発（blowup）の証明を生成したと公表した。同社は理論文書とともに、公開リポジトリNavierStokesAndEulerを提示した。そこには、外部強制項の下にある滑らかな初期データに関する定理を、Lean 4で形式化したものが収められている。研究所自身の説明によれば、この結果は数学者チャールズ・フェファーマンがクレイ数学研究所のために起草した定式化のうち、正則性の破綻に関する主張をカバーしている。ただし外力を持たない場合は扱っておらず、科学界はそちらこそがこの問題のより難しい変種だと見ている。公式な定式化の起草者は今回の解決を胸躍るものだと評し、コルドバとマルティネス=ソロアの寄与に言及した。一方で同社は当初から、100万ドルの賞金を請求するつもりはないと明言している。

この出来事は、数学の自動化と学術機関の時間感覚とを絡み合わせている。クレイ数学研究所は依然としてナビエ–ストークスを未解決問題として掲載している。規定は、資格のある媒体での公表、公表から少なくとも2年の待機、そして数学界による一般的な受容を求めており、研究所は現時点で内容についての判断を示していない。同研究所のマーティン・ブリッドソン所長は、評価は絶対的な厳密さを担保するために、意図的に急がない歩みをとると述べている。図式をさらに込み入らせているのが、先取権をめぐる論争である。数学者テレンス・タオが紹介した並行する研究があり、著者たち自身がそれを人工知能に大きく助けられたものだと説明している。ニューヨーク大学のある数学者は、研究所が示した接触経緯の説明に異議を唱え、プロプライエタリなツールの非公開セッションが結果に寄与した可能性を指摘した。同社は未公開の研究を直接見たことを否定しつつ、非識別化された利用データが自社モデルの学習に影響した可能性は排除できないと認めている。

リポジトリには、証明を機械に再検査させるための手順が示されている。しかし独立した検証はこれまでのところ完了していない。しかもその検査を別にすれば、用いられたインフラがプロプライエタリであることが、コストや誇示された効率指標についてのいかなる独立検証も阻んでいる。公表された計算量——9月1日から5日にかけて約1万のエージェントを並行稼働させ、証明に至るまで88時間、Leanでの形式化と検証にさらに17時間——は、外部の誰にも再現できない企業側の主張にとどまる。学習コードにもシステムの重みにもアクセスできない以上、科学界が確認できるのはリポジトリに預けられた形式的な手順だけであり、実験の再現可能性の実態は影のなかに残される。

形式数学は、論理の各段階を自動で検査する強力な味方を得た。しかし閉じたモデルによる科学的先陣争いは、その構造的な限界を露呈している。定理を検証することは、いまや機械が実行できる作業だ。それを生み出した工程の透明性を見極める作業のほうは、依然として完全に人間的な厳密さを要求する。

— Olya