OpenAI、社内フロンティアモデルの数学的成果を論文アーキテクチャとして公開──GitHubに722本の原稿と形式証明を収録
リーマン予想の関連難問を含む未解決問題の検証結果722本をGitHubで公開し、Leanによる形式証明や計算コストを開示した。
リリース: 2026-10-07 · 読了 4 分記事の要約
1. 核心（What）
- 米OpenAIは10月6日（現地時間）、社内フロンティアモデルが生み出した数学の成果として、論文の原稿や証明支援系「Lean」による形式証明など722本をGitHubで公開した。
- 評価期間中にモデルに与えた問題は約4,000問であり、一定の重要性を満たすものに絞り込んで722本に選定したとしている。
- 大半の論文は未公開の同一モデルを使用し、1件当たりの平均計算量は「ChatGPT Pro」の思考機能を約3時間使った分に相当する。
- 数学者らの独立組織「AGMAI」の提言に基づき、推論過程の要約10件分や、所要時間・計算コストが開示されている。
2. 影響（Why）
- AIによる数学的発見の検証可能性向上: 社内モデルの成果がLeanによる形式証明やGitHubリポジトリで開示されることで、第三者の研究者が追試・検証できる基盤が整った。
- 国内数理研究組織への影響: 数理最適化や自動定理証明を扱う国内の研究機関や大学の研究室は、公開された722本の形式証明データセットをLLMの数学推論能力の新たなベンチマークとして活用できる。
3. 根拠・詳細（How）
- Leanによる形式証明とGitHubリポジトリによる公開: 証明支援系「Lean」を用いた形式証明を多くの原稿に付与し、AGMAIの提言に沿って外部リポジトリであるGitHub上で722本の原稿を配布した。
- 計算コストと推論プロセスの開示仕様: 1件当たりの計算量をChatGPT Proの思考機能約3時間分に換算し、円周率の無理数度やマーラー予想など10件の推論過程要約を併せて公開した。
4. 展望・課題（Next）
- コミュニティ主導の公開プラットフォーム検討: 今後はGitHub以外のコミュニティ運営の公開先も検討し、先行研究の引用や数学的な説明方法を改善していく方針。
- 数学者向け特別プログラムと一般提供: AIの成果を数学者が理解するためのワークショップ等に資金提供を行い、成果を出したモデルの責任ある一般提供に向けて取り組む。