OpenAIが公開した数学成果は、生成の量が検証の速度を追い越した最初の大規模な実例になった。READMEが示す形式化率は約42%で、残りは人間が読んで確かめるしかない。数学者や査読者にとっては、AIが出した論文を「読む」作業そのものがボトルネックになる。AIが研究成果を自律的に出す流れが続くほど、本当の問いは「何が証明されたか」から「誰が、どの速度で、それを確かめるのか」へ移る。
何が起きたか
OpenAIは、内部の未公開モデルによる数学成果をGitHubリポジトリ openai/math で公開した。出回った「377件」という数字は、公式READMEと合わない。READMEは「現在のカタログは719本の原稿を372のファミリーに整理している」と記す。二次報道は722本と伝えており、原稿数は取得時点で719と722が混在する(更新による差とみられる)。本記事は公式に従い「372ファミリー」を用いる。数値は取得時点のものである。
仕組み・詳細
- モデル: READMEによれば、結果の大半は同一の手順で、OpenAIの未公開内部モデルを使って得られた。「大半」であり全件ではない。
- 推論の要約: 10ファミリー分について、モデルの推論の要約(abridged summaries)が収録されている。
- 形式化: トップライン結果の約42%がLeanで形式化されている。未形式化分の一部には問題がありうるという注意書きがある(二次報道経由)。
数字で見る
| 項目 | 数値 | 出典 |
|---|---|---|
| 結果ファミリー数 | 372 | 公式README |
| 原稿数 | 719(二次報道は722) | 公式README/二次報道 |
| 提示した問題数 | 約4,000 | 公式README |
| 1結果あたりの計算量 | 平均でChatGPT Pro思考計算 約3時間 | 公式README |
| Lean形式化済み | トップライン結果の約42% | 公式README |
計算量はChatGPT Proの利用量換算の見積もりである。約4,000問を投げて372ファミリーを得たことになり、大量に試行して通ったものを拾う構図だと読める。ただし、そこから成功率を算出する根拠はREADMEにない。
背景
自律的に研究成果を出す事例は、暗号解読や数学で相次いでいる。数学では、長年未解決の問題へのAIの解答や、Leanによる形式検証の事例が積み上がってきた。今回の公開は、個別の大きな成果ではなく、ファミリー単位のカタログとして量で出された点が特徴である。形式検証が付いた約42%は機械が正しさを保証し、付かない部分は人の確認に依存する。
なぜ重要か
- 読む側のコスト: 成果が増えても、未形式化分は専門家が読まなければ正否が分からない。
- 評価の分離: 公開数と、検証された正しさ・数学的な価値は別の指標である。本記事は成果の質(新規性や重要度)を確認できていない。
未検証・留意点
- 公式ブログ(発表日や公開方針の説明)は取得できず、発表日は2026-10-06頃とされるが未検証。
- 取り上げられた分野(代数、数論、理論計算機科学、論理、位相幾何)のうち、READMEで確認できたのは数論・組合せ論・代数・解析・物理関連数学という程度で、論理と位相幾何の明記は確認できていない。
- 数学者の間で、創造的な思考なのか既存の着想を借りた最終証明の仕上げなのかという議論がある、との見方は一次ソースで確認できていない。二次報道には、フィールズ賞受賞者らが概念的理解の欠如や文献の急増を懸念するという内容があるが、論点は「創造性か仕上げか」より別の所にあり、ここでは事実として扱わない。
- 準リーマン予想や行列積指数の上界などの成果の質は、二次報道の記述で一次未検証。