10月6日、OpenAIが「Sharing AI progress in mathematics」と題した記事を公開した。社内の最先端モデルが「幅広い新しい数学的結果」を大量に生成したとし、その成果をGitHubリポジトリで公開。さらに多くの証明にはLeanによる形式検証を同梱しており、「AIが本当に正しい証明を出したのか」を機械的に確認できる形で提供している点が技術的に際立っている。数学の新定理発見は研究者の数年分の仕事に相当することも珍しくない分野だけに、AIがそれを大量生成したという今回の発表は、数学コミュニティへの影響という意味で見過ごせない内容だ。
AIが数学の新定理を大量生成——OpenAIが成果を公開
OpenAIは、社内のフロンティアモデルが生成した幅広い新しい数学的結果を公開した。このモデルは、同社が別途取り組みを公表しているNavier-Stokes方程式（流体力学の根本方程式であり、その解の存在と滑らかさはミレニアム懸賞問題のひとつとして知られる）への応用にも使用されているフロンティアモデルと同系統のものだ。今回の公開は、そのモデルが生成した成果を数学コミュニティと共有する取り組みの第一弾に位置づけられる。
数学AIの文脈では、DeepMindが2024年に発表したAlphaProofがLeanを活用してIMO（国際数学オリンピック）問題を銀メダルレベルで解いたことが大きな話題となった。OpenAIの今回の取り組みはIMOのような競技問題への挑戦にとどまらず、「新しい数学的結果の大量生成と公開」という方向性を打ち出しており、数学AI研究の競争が新たな局面に入ったことを示している。
計算コストの目安：ChatGPT Proで平均約3時間分
今回の公開で特に具体的な数字として示されているのが、計算コストの見積もりだ。
各結果の生成に要した計算量は「ChatGPT ProのThinking機能換算で平均約3時間分」と記されている。Proプランの月額コストを考えると、数学の新成果1件あたりの計算コストがどの程度のオーダーかを、研究者が肌感覚で把握しやすい形で示している点は実用的だ。
公開されているリポジトリには、以下の情報が含まれる：
- モデルの推論過程のサマリー（10件）——これは推論過程の「代表例」として抜粋公開されているものであり、生成された定理の総数とは別に読む必要がある
- ChatGPT Pro利用量換算での計算コスト推定
- 試行した問題数に関する統計
Leanによる証明の形式検証を同梱
技術的に特筆すべきは、多くの証明についてLean（コンピュータが数学的証明を機械的に検証できるプログラミング言語）による形式化（formalization）を一緒に公開している点だ。
Leanはここ数年、数学コミュニティとAI研究者の間で急速に注目を集めている証明支援系（proof assistant）で、DeepMindのAlphaProofもLeanを活用して話題になった。形式化された証明があれば、「AIが本当に正しい証明を出したのか」を人間が一から追わなくても機械的に確認できる。
OpenAIは「今後、形式化が完了したものから順次リポジトリを更新する」としており、全件が即座に検証可能な状態ではない点は留意が必要だ。
公開方法：AGMAIの助言を受けて設計
成果の公開方法については、AGMAI（数学とAIに関する独立諮問グループ）と協議しながら策定した。AGMAIはプリンストン高等研究所（IAS）の支援のもとに設立された独立組織であり、AIと数学の交差点における倫理・実務上の指針を提言している。同グループの公開提言を踏まえ、今回はGitHubリポジトリでの公開を採用。論文改訂や引用のためのプロトコルも整備されている。
OpenAIは「今後のリリースでは、引用・数学的説明・結果の提示の質をさらに向上させる」と明言している。
今後の展開
OpenAIは以下の方針も示している：
- AIが生成した主要な数学的成果の理解を深めるためのワークショップ・学会・特別プログラムへの資金提供（詳細は近日公表予定）
- 今回の成果を生成したモデル自体の責任ある公開に向けた取り組み
- コミュニティからのフィードバックを反映した、科学的進歩の開示基準の継続的な更新
数学や他の科学分野での内部フロンティアモデルの評価を継続することで、各分野を前進させるツールの開発を加速させる狙いだとしている。
詳細はSharing AI progress in mathematicsを参照していただきたい。
