OpenAIは、未公開の内部モデルが生成した722件の数学原稿を公開した。同社はこの成果を、大部分が単一のプロンプトを単一のエージェントに与えて得られたものだと説明している。原稿は372の関連結果のファミリーに整理されているが、数学者らは、モデル、プロンプト、その他の証拠が公開されるまで、これらの主張を完全に評価することはできないとしている。

今回の公開は、AI研究所がフロンティアモデルの推論能力の試金石として数学を活用する動きが強まる中で行われたものであり、AI生成の研究成果をどう公開・検証・開示すべきかを試す早期の事例となりつつある。

OpenAIの広報担当者は、そのほとんどが単一のAIエージェントに与えられた単一のプロンプトから生まれたものだが、一部は複数回の試行を要した可能性があると述べた。同社は、モデルに約4,000問を提示し、公表に値すると判断した出力を選択したと説明している。

MITの数学者アンドリュー・サザーランドはScientific Americanに、この「一発解決」の主張は慎重に扱うべきだと語った。「彼らがモデルを公開し、人々が結果を再現できるようらない限り、単一のエージェントによる問題の一発解決に関する主張はすべて未検証として扱うべきだ」とサザーランドは述べ、「証拠を求めるべきだ」と付け加えた。

722という数字は解決された問題の数ではなく、原稿の数を表している。結果のファミリーには、主定理に加えて補足的な議論、帰結、あるいは別証明が含まれる場合がある。OpenAIによると、平均的な結果にはChatGPT Proの思考計算に換算して約3時間が使用されたという。これは先月のナビエ・ストークス方程式に関する主張とは大きく異なり、そちらでは1万個のエージェントが連携して88時間作業した。

OpenAIは10件の結果について要約された推論サマリーを公開した。しかし、GitHubリポジトリ内の形式化カタログによると、722件の原稿のうちコンピュータ検証済みの主結果を含むのは現在162件のみである。これは全体の約22%に相当し、結果がLean（各論理ステップを機械的に検証するソフトウェア）に翻訳されていることを意味する。Leanは数学における機械検証証明の事実上の標準となっており、そのため約560件のまだ形式化されていない原稿が、この成果集の最大の未解決課題となっている。

OpenAIは、すべての原稿にLean形式化があるわけではなく、「一部の未形式化の結果には問題がある可能性がある」と警告している。Lean検証に合格したことは、証明がLeanに書かれた命題から導かれることのみを確認するものである。命題が元の問題と一致するか、結果が新しいか重要かは証明されない。これらの問いには依然として数学者による検討が必要である。

研究者らはすでに、資料そのものとその公開方法について懸念を表明している。ドミトリー・ルービンはXで次のように書いた。

I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026

キース・アドラーはXで次のように書いた。

The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithadler) October 7, 2026

ニュージャージー州プリンストンの高等研究所も、AI生成の数学的成果がもたらす影響に疑問を呈した。「AIが、プロンプトを与えた人間がその議論を理解、検証、あるいは責任を負うことができない状況で、数学的議論を出力できるようになったのが現状です」と同研究所は声明で述べた。「数学に対する人間の理解が依然として最も重要であると我々は考えています。この新時代において、数学に対する人間の理解を責任ある学術的成果の一部として含む新しいパラダイムに向けて、どう取り組めばよいのでしょうか」

一方、アビシェック・サハ教授はより肯定的な見方を示し、「数学にとって非常に大きな日だ」と書いた。その上で、結果の大部分は「既存のプログラム内での卓越した進展」や「驚くべきブレークスルー」といったカテゴリーに該当すると指摘した。彼の評価によれば、この成果集には興味深い問題は含まれているものの、クレイ数学研究所の100万ドル懸賞問題であるミレニアム問題に匹敵する結果はない。そして722件の中でその水準に達したのはただ一つ、擬リーマン予想だけだと特定した。

サハはXで次のように書いた。

Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… — Abhishek Saha (@ObhishekSaha) October 7, 2026

今回の公開は、9月29日に高等研究所の諮問グループが出した推奨事項にも及ばなかった。同グループは、モデル名、プロンプト、要約された思考連鎖、所要時間、各結果の計算コストの開示を推奨していた。OpenAIは平均的な計算数値と10件の推論サマリーを提供したが、プロンプトは公開しなかった。同社は、責任ある形でモデルを公開できるよう引き続き取り組んでいるとしている。

トロント大学の数学者ダニエル・リットは逆の立場を取り、これらの数学の問題の答えを秘密にしろとOpenAIに求める理由はないと主張した。

Anthropicは先月、異なるアプローチを選択し、フェルマ最終定理のLean検証済み証明全1,300万行をGitHubで公開した。この成果は、1995年にアンドリュー・ワイルズが発表した定理を形式化したものであり、新しい数学的結果を主張するものではなかった。この2つの公開は、業界における開示戦略の分裂を示している。一方には既知の定理の完全な機械検証証明が、他方には部分的な形式的検証にとどまる大量の新たな主張がある。

OpenAIは、Lean形式化が入手でき次第追加していくと述べている。現時点で、722件の原稿のうち形式化された主結果を持つのは162件である。残りの原稿の評価は、研究者らが最も必要としているもの、すなわちモデルの公開、元のプロンプト、そして残りの原稿の独立した形式化にかかっている。