OpenAI、Navier–Stokes方程式の特異性証明とLean証明書を公開――数学界による検証は始まったばかり

OpenAIは9月8日、社内モデルが生成したNavier–Stokes方程式に関する証明を公開し、Clay Mathematics Instituteによる問題記述の反例ルートCおよびDを完成させたと主張した。この構成は、滑らかで有限エネルギーの三次元非圧縮性流れから出発し、滑らかさを保つ外力を加えることで、渦核を継続的に内側へ収縮させながら軸方向に伸長させる。速度や方程式中の一部の項は非有界へ向かう一方、移流、圧力、粘性などの成分を精密に相殺することで、外力自体が特異になることを回避する。議論が正しければ、この結果は、少なくとも一部の許容されるデータについて大域的な滑らかな解を維持できないことを意味するものであり、一般的な流体シミュレーションに対する閉形式解を提供するものではない。

この技術ニュースにおけるもう一つの焦点は、成果の提供形態だ。GitHubリポジトリには、全空間と周期トーラスをそれぞれ扱うLean証明が収録され、Lean 4.34.0-rc2、Mathlib、Lakeの各バージョンが固定されている。第三者は依存関係のキャッシュをダウンロードした後、`lake build`を実行できるほか、独立検査用のComparatorチャレンジも用意されている。自然言語の論文だけを公開する場合に比べ、欠落した補題、密かに追加された公理、型の不整合を発見しやすい。ただし、Leanのカーネルが確認できるのは、プログラムから形式化された定理が確かに導出されることだけだ。形式的な命題が元のミレニアム懸賞問題に完全に対応しているかを自ら判定することはできず、数学的構成や引用元に対する審査の代わりにもならない。

OpenAIによると、このシステムでは多数の協調エージェントが、キャッシュされたWebデータとプログラミングツールを利用し、関連研究の噂を耳にした後、集中的な探索を行ったという。使用された基盤モデルは依然として非公開であり、訓練データ、エージェントの軌跡、探索コスト、失敗した試行についても、再現に必要な情報が十分に開示されていない。したがって現時点では、解決が確認された案件ではなく、実行可能な証明書が付属する重要な証明候補とみなすべきだ。Clay Mathematics Instituteの規則では、成果が適格な出版媒体に掲載されてから少なくとも2年が経過し、世界の数学界から広く受け入れられた後でなければ、正式な検討対象にならない。今後最も注目すべき点は、独立したLean環境での再構築、解析学者による形式化と論文との対応関係の逐次検証、そして形式的な命題の枠外に置かれた暗黙の仮定を公開審査が発見できるかどうかである。