OpenAI、AI数学手稿722篇を公開――最大規模公開ベンチマークの背後にある透明性をめぐる攻防

2026年10月7日 20 約10分 News Factory

OpenAI 数学推理 Lean形式化证明 AI研究透明度前沿模型 AGMAI 黎曼猜想

2026年10月6日、OpenAIはGitHub上にopenai/mathという公開リポジトリを立ち上げ、Apache-2.0ライセンスのもと722篇の数学手稿を公開した。372の問題族に分類され、Lean形式化証明ファイルとモデル推論サマリーが付属している。これらの成果を生み出したのは非公開の内部先端モデルであり、複数の独立した報道によれば、その能力はGPT-6 Astraを大幅に上回るとされる。これは現時点で最大規模のAI数学出力公開集となる。

手稿の生成プロセスは比較的固定されており、モデルに約4000問の開放型数学問題を入力し、顕著性によるスクリーニングと成果のグループ化を経て、最終的に722篇の手稿が生成された。OpenAIは、採用された成果1件あたりの平均計算コストは約3時間のChatGPT Pro思考に相当すると明らかにしている。

4つの主要成果――含有量にはばらつき

中国語メディアなどの技術的整理によれば、今回の手稿の中で数学界から最も注目を集めているのは次の4分野である。

準リーマン予想（Quasi-Riemann）：手稿は、リーマンゼータ関数が実部7/8より大きい領域に零点を持たないことを証明したと主張している。ラトガーズ大学の数学教授Alex Kontorovichはこの結果を見て、「人間が証明したなら即座にフィールズ賞、それは間違いない」と公言した。完全なリーマン予想の解決には至っていないものの、この固定幅の零点禁止領域の拡張は技術的に従来の予想をはるかに超えると評価されている。この成果にはLean形式化資料が付属している。
ホッジ予想の特殊ケース：CM型アーベル多様体上の有理ホッジ予想の証明を提示している。ホッジ予想はミレニアム懸賞問題の一つであり、今回はその特殊かつ重要なケースを扱っているが、完全なLean形式化は未完成である。
ユニークゲーム予想（Unique Games Conjecture）：手稿は証明を主張し、そこからMax-Cutなどの問題の近似困難性の下界を導いている。P≠NPを前提とすると、特定の計算問題における効率的アルゴリズムの近似保証が対応する理論的下界を突破できないことを意味する。
自由群因子問題：パラメータが1より大きいすべての補間自由群因子（無限パラメータの場合を含む）に関する結論を提示しており、Lean形式化資料が付属している。

リポジトリのREADMEには2件の例外も記載されている。リーマンゼータ関数関連の手稿とホッジ予想の手稿は、固定プロセスから逸脱した唯一の2篇であり、リーマンゼータ関数の手稿は可読性向上のため人手による編集が加えられている。

Lean形式化――検証の基準だが、カバレッジは限定的

今回の公開において、Lean形式化証明は技術的信頼性の中核的な根拠となっている。Leanはコンピュータが数学的証明を逐一検査できるプログラミング言語であり、「明らかに成立する」という飛躍を許さず、すべての推論ステップが論理規則によって検証される必要がある。

公開ディレクトリの統計によれば、722篇のうち主要結論にLean形式化資料が付属しているのは約162篇に留まり、残りはコンピュータによる検証が未完了である。OpenAIはREADMEで、形式化されていない一部の結果に問題が存在する可能性を認め、継続的な改訂を約束している。リポジトリに含まれるモデル推論プロセスのサマリーはわずか10件であり、全量の推論チェーンではないため、研究者が各結論の生成ロジックを体系的に追跡することはできない。

コーネル大学数学准教授のDaniel Halpern-Leistnerは自動形式化ツールを開発中であり、かつてメディアに対して「自然言語で書かれた論証が大量に流入しているため、この作業は今や非常に緊急性が高い」と述べた。同時に彼は、コンピュータが検査するのはコード内で定義された命題であり、コードの定義と元の数学的問題との間にずれがあれば形式化の通過は論文全体を保証しない、という重要な境界線も指摘した。準リーマン成果のLean説明書も、論文の後続応用部分はその形式化の対象範囲外であると明記している。

これはLean形式化の否定ではなく、その限界の正確な記述である。Lean形式化は現時点でAI数学出力の最も厳格な検証メカニズムであるが、「主要結論にLeanあり」と「論文中のすべての結論が信頼できる」との間には依然として実質的な開きがある。

AGMAI――半ば強制的に介入した学術ガバナンス

今回の公開の背後には、これまでほとんど注目されてこなかったガバナンスメカニズム――AGMAI（数学と人工知能に関する諮問グループ）――が存在する。プリンストン高等研究院（IAS）が主宰し、フィールズ賞受賞者のTimothy Gowers、Martin Hairer、Edward Wittenら数学界の第一人者が参加している。

AGMAIの誕生自体に受動的な側面がある。今年9月初め、OpenAIはNavier-Stokes関連成果の公開方法について学術界から批判を受け、その後IASと協力してこの諮問メカニズムを設立した。AGMAIは9月29日に責任ある公開に向けた勧告を正式発表した。この勧告は数学界からの600件以上の回答を体系的に整理したものであり、主な内容として、AI機関が数学的成果を公開する際はモデル名、プロンプト、推論サマリー、計算コストを開示し、論文を「いかなるAI企業の管理下にもない学術リポジトリ」にアーカイブするよう求めている。

AGMAIはとりわけ、数学的成果の公開をモデルのマーケティングツールとして利用することを名指しで警告し、そのような行為は「数学界に重大な損害をもたらした」と述べた。

この警告には背景がある。複数の報道によれば、今年8月にOpenAIは約40人の数学者を非公開会議に招集し、モデルがすでに数百の難問を解いたことを示唆した。会議の参加者の中には、同社が成果を一度にまとめて公開しないと約束したと受け取った人物もいたが、OpenAIの広報担当者はその後、そのような約束があったとは承知していないと述べた。双方は約束が存在したかどうかについてそもそも合意に達していない。

10月6日の今回の公開は、規模においても透明性の基準においても、8月の論争的な公開と鮮明な対比をなしている。OpenAIはリポジトリにバージョン管理メカニズムを設け、すべての改訂履歴を記録し、旧バージョンへのアクセスを保持し、各手稿にBibTeX引用フォーマットを提供している。これは学術標準の基本仕様だが、AI企業主導の研究公開では一般的ではない。

標準ベンチマーク飽和の後

OpenAIはREADMEの中で、今回の手稿の評価的背景を説明している。既存の数学評価セットにおけるモデルの性能はすでに飽和に近づいており、評価チームはより多くの開放型数学研究問題をテストに組み込まざるを得なくなっている。これはAI能力追跡の領域において構造的な意義を持つシグナルである。標準化ベンチマークがトップモデルを区別できなくなったとき、信頼できる最前線の評価をいかに設計するか自体が、解決すべき方法論的問題となっている。

今回公開された722篇の手稿は、この問題に対して新たな参照系を提供するものである。再現可能で引用可能、かつ部分的に形式化検証が可能な実際の開放型数学問題集であり、372の問題族が数学分野ごとに分類されている。各問題族の内部には主要結論、付随する論証、系、および代替証明が含まれ、研究者が異なる角度から検証を切り出すことができる。これは従来のAI数学能力の展示方法――主にコンテスト問題集や閉鎖型評価に頼るもの――とは質的に異なる。

ノースウェスタン大学の数学者Bryna Kraは公開前にWIREDの取材に応じ、「これは不安な瞬間だが、同時に本当にエキサイティングでもある」と語った。

独自評価

今回の公開の意義は数学的成果そのものの価値にとどまらず、一つの先例を確立した点にある。AI機関が学術諮問の枠組みのもと、引用可能でバージョン追跡が可能、かつ形式化検証を経た形で先端モデルの推論出力を公開できることを示した。このメカニズムが他のAI機関にも複製されれば、AI出力の学術的信頼性に向けた構造的な通路が形成されることになる。

今回の公開には、引き続き注視すべき2点がある。第一に、Lean形式化のカバレッジのギャップは実質的なものであり、722篇のうち約560篇はまだコンピュータ検証が完了しておらず、形式化されていない結果に系統的な問題が存在するかどうかは現時点では排除できない。第二に、AGMAIが求めた「独立した学術リポジトリ」へのアーカイブはまだ完全には実現していない。OpenAIが選択したのは自社が管理するGitHubリポジトリであり、技術的な開放性の要件は満たすが、機関としての独立性においてはAGMAIの理想的な基準とまだ距離がある。

再現可能で検証可能なAI数学出力は、本日をもって最大規模の公開ベンチマークを手にした。これは確かな技術的前進である。次の問いは、数学界が372の問題族の独立した評価をどれほどの速度で完了できるかにかかっている。その速度が、これらの手稿が最終的に学術共同体に有効な知識として受け入れられるかどうかを決定するだろう。