OpenAI、社内フロンティアモデルによる新たな数学的成果を一括公開：Lean形式化と計算量の開示付き
2026年10月6日、OpenAIは社内のフロンティアモデルが生み出した新たな数学的成果を幅広く公開した。成果はGitHubリポジトリに置かれ、論文の改訂と引用の手順が添えられ、多くの証明にはLean形式化が付く。モデルの推論要約10件、ChatGPT Proの利用量換算による計算量の推定、挑戦した問題数の統計も公開された。平均的な成果は約3時間分のChatGPT Pro推論に相当する計算量を使った。公開方法は高等研究所（IAS）の独立諮問グループの助言を踏まえている。
発表の内容 2026年10月6日、OpenAIは研究記事「Sharing AI progress in mathematics」を公開し、社内のフロンティアモデルが生み出した新たな数学的成果を幅広く発表した。ポイントは「幅広く」という点だ。単一の論文や定理ではなく、成果の集合である。OpenAIはそれをGitHubリポジトリに置き、論文の改訂と引用の手順を添えた。記事は、諮問委員会の指針に合うコミュニティ運営の代替先も引き続き探していると述べている。 最初に範囲を明確にしておく。原文は個別の定理名を挙げておらず、解決した問題の総数も示していない。示されているのは、公開方法、開示内容、そして平均的な計算量の数字である。本稿はこれらの公開情報だけに基づき、数学的内容そのものについては推測しない。 公開手順：数学界の規範に近づける 今回の公開で最も興味深いのは手順である。OpenAIは、数学コミュニティへの成果共有の方法を改善するため、高等研究所（IAS）の独立した「数学と人工知能に関する諮問グループ」に相談したと述べている。公開方法はその助言と公開されている提言を踏まえて決めたという。
これが重要なのは実務上の理由による。数学には、発表、功績の帰属、査読について独自の伝統がある。AI企業が「当社のモデルがこれを証明した」とブログに書くだけでは、数学者は真偽を判断しにくく、引用の仕方も分からない。改訂と引用の手順を備えたリポジトリに置くことは、成果がコミュニティによる確認、訂正、正式な引用を必要とすると認めることでもある。OpenAIは今後の公開でも、引用、数学的な説明、結果の見せ方を改善し、読者が理解しやすくすると約束している。 Lean形式化：機械に証明を検査させる リポジトリのもう一つの柱は、多くの証明に付くLean形式化である。Leanは、数学の証明が正しいかどうかを計算機が一歩ずつ検査できるプログラミング言語だ。 AIが生成する数学では、これが特に重要になる。言語モデルは、厳密に読めるのに微妙な欠陥を含む議論を書くことがあり、人間の査読は遅くて費用もかかる。形式証明は証明検査器が一行ずつ確認する。形式化された主張が元の問題と一致していれば、証明そのものを信頼に頼る必要はない。そうなればコミュニティは、形式的な主張が元の問題を本当に捉えているか、その結果に数学的な価値があるか、という、より難しい二つの問いに力を注げる。
OpenAIは、形式化が得られしだいリポジトリを更新すると明言している。つまり現時点ですべての成果が形式化されているわけではない。読者はリポジトリの現状を基準にするべきだ。 透明性：推論要約、計算量、挑戦回数 成果そのもの以外にも、OpenAIはどのように得たかについての詳細を公開した。モデルの推論要約10件、ChatGPT Proの利用量に換算した計算量の推定、挑戦した問題数の統計である。公表された平均は、1件の成果あたり約3時間分のChatGPT Pro推論に相当する計算量だ。 三つの開示はそれぞれ役割が違う。推論要約は、モデルがどう結論に至ったかを外部が見る手がかりになる。計算量の推定は、1件の成果にかかるコストの桁を示し、AI研究の経済性を評価する上で欠かせない。挑戦数の統計は古い問いに答える。目にする成功の裏に、どれだけの失敗があるのか。分母のない成功率は意味が薄く、分母を公開するのは珍しい誠実さである。 ただし注意点がある。「3時間分のChatGPT Pro推論」はOpenAI独自の換算単位であり、GPU時間の実数ではない。外部から正確なコストを再計算することはできない。 科学界と業界にとっての意味 数学者にとっては、直接検討できる資料群である。論文、証明、統計が一か所にまとまり、改訂と引用の経路も定められている。AI業界にとっては、開示のひな形になる。成果、形式証明、計算量の記録、失敗の統計をそろえる形だ。今後、他社が同様の進展を発表したとき、読者は同じ問いを投げる根拠を持つ。
企業にとってのシグナルは単純ではない。一方では、長時間推論を行うフロンティアモデルが、検証可能で研究水準の出力を作れることを示す。他方でOpenAIは、これらの成果を生んだモデルを責任ある形で公開すべく取り組んでいる、と述べるだけで、時期は示していない。したがって、提供済みの製品機能とみなすべきではない。 今後と課題 OpenAIは、AIが生んだ重要な成果の理解を目的とするワークショップ、会議、特別プログラムを資金面で支援すると述べ、詳細は近く共有するとしている。実務的なシグナルである。機械が出した証明を理解することは、それ自体が人の仕事であり、ボトルネックは結果を出すことから、結果を消化することへ移りつつある。また同社は、科学者に最先端の能力を直接届けたいとし、社内のフロンティアモデルを数学などの科学で評価し続けることが、各分野を前進させる道具づくりにつながると述べている。 課題も明らかだ。第一に、形式化が成果の増加に追いつくか。第二に、形式的な主張が意図した問題の忠実な翻訳であるかは、今も人が確認する必要がある。第三に、功績、著者性、責任を人とモデルでどう分けるかについて、数学界に定まった見解はない。第四に、一度きりの公開が定着するかは、OpenAIが約束どおり基準を更新し、コミュニティの声に応え続けるかどうかにかかる。 総じて、この公開の価値は数学の内容だけではない。AIの研究成果について、検証でき、引用でき、訂正できる開示規範を作ろうとする試みにある。その規範が持ちこたえるかどうかは、今後数か月のコミュニティによる検討の結果次第である。