OpenAIが社内AIの数学論文722本を公開372件を難しさ順に並べ、取り上げた問題のLean証明を手元のMacで照合した

2026年10月7日・日本時間時点の情報です。OpenAIは10月6日（米国時間）、まだ公開していない社内のAIが書いた数学の論文722本を、372件の「ファミリー」にまとめてGitHub（openai/math）で公開した。9月21日に「100以上の未解決問題を解いた」と発表していた社内モデルの結果で、Scientific Americanは「同じモデルによる372件の結果」と伝えている。この記事は、372件のうち看板級の問題を4つの物差しで並べ、取り上げた問題に付いているLeanの証明を、筆者の手元のMacで公式の照合ツールにかけた結果をまとめたものだ。

動画版（約20分・黒板で並べたランキング）： https://youtu.be/HXONhWG85Ww

3行まとめ

1. 公開されたのは論文722本・372件・PDF合計3万4815ページ。論文に書かれた日付は9月10日〜10月6日に収まり、9月24日だけで194本。OpenAIのREADMEによると約4,000問を出題して372件に絞り、1件あたりの計算は平均でChatGPT Pro約3時間分。372件中235件にLeanの証明が付いている。
2. S段（世界の看板問題）には、リーマン予想の弱い形（実部7/8より右にゼロが無い）、BSD予想・ホッジ予想の一部、ヒルベルト第16問題、有理数上のヒルベルト第10問題、Unique Games予想が並ぶ。ミレニアム懸賞の3問はどれも「一部分」の主張で、すべてOpenAIの主張・人間の査読はまだ。
3. 取り上げた問題のLeanの照合用ファイル36個を、OpenAIの設定のまま公式の照合ツール comparator で確かめた。36個すべてが合格した（隔離の部品を代わりのものにした点を除き、公式の手順どおり）。

何が公開されたのか

OpenAIの広報はScientific Americanに対し、ほぼ全部が1つのAIエージェントへの1回の依頼で得られた結果だと説明している（一部は複数回試したとも述べている）。9月のナビエ・ストークスは、同誌によると約1万体のエージェントを使い、数百万ドル規模の計算だった。

4週間で722本──人間の記録と並べると

論文フォルダの日付を1本ずつ数えると、9月23日に177本、9月24日に194本、10月5日に112本だった。合計は722本・3万4815ページ。

arXiv全体でも、9月の投稿は2024年の20,569本から2026年の40,363本へ増えた。arXivは公式ブログで「高度なAIツールがこの増加を押し上げている」と書き、10月1日から1人あたりの投稿を月2本までに制限した。なお、OpenAIの論文はarXivではなくGitHubに出ているので、この2つは別々の事実として並べている。

難しさ・すごさで並べると

物差しは4つにした。①有名な問題リスト（ミレニアム懸賞・ヒルベルトの23問題・スメールの問題・サイモンの問題・エルデシュの懸賞・Wikipediaの未解決問題リスト）に載っているか、②出された年、③丸ごと解いたのか一部分か反例か、④Leanで機械検証されているか。段の分け方はこの4つを見た筆者の判断だ。

S段：世界の看板問題

A段：名前の付いた予想を丸ごと解いたという主張（抜粋）

トンプソン群Fは従順でない（1979年に出された問い）／自由群因子の同型（作用素環で最も有名とも言われる問題で、多くの専門家は「同型でない」と見ていた。OpenAIの答えは「同型」）／カディソンの相似問題（1955年）／キャノン予想／カプランスキーの零因子予想に反例／エルデシュが5,000ドルの懸賞をかけた等差数列の予想／πの無理数度は2（これまでの上限は7.103）／カタラン定数は無理数／マーラー予想／ファルコナーの距離予想／アンダーソン局在とハイゼンベルク強磁性体の自発磁化（サイモンの問題）／シドレンコ予想に35頂点・66辺の反例／バーネット予想（1969年）／3次元格子の臨界パーコレーション

B段：記録の大幅な更新

手元のMacでLeanの証明を照合した

リポジトリを開いた時点で、容量2.3GB・ファイル13万2851個・論文3万4815ページだった。筆者は量で読むのを諦め、読むのはAIに任せた。372件の題目を全部抜き出させ、看板級の90件を4体のAIに分けて下調べさせたところ、4体とも約4分で終わった。ただ、その下調べには記憶で書いた年や記録がかなり混ざっていたので、別のAIに30項目の裏取りをさせ、数字と年は一次資料を開いて確かめたものだけをこの記事と動画で使っている。

Leanの証明は、取り上げた21件に付いている照合用ファイル36個を、OpenAIが用意した設定のまま公式の照合ツール comparator にかけた。合格の条件は、照合用の問題文と同じ文を証明していること、使っている公理が標準の3つ（propext・Classical.choice・Quot.sound）だけであること、Leanの中核が証明を受け入れること、の3つ。

※ かかった時間は、照合ツールが組み立て・書き出し・検査にかけた時間。2つの照合と動画の書き出しを同じMacで並行して回した時間を含む

最初に確かめたトンプソン群Fは、OpenAIのLeanファイル68個（約9,500行）を組み立て直して25秒で通り、照合用の定義は1文字も違わなかった。比べるために、証明の最後の1行で掛け算の順番を入れ替えた版も作ると、Leanは「Type mismatch」で止めた。準リーマン予想の1件は、たどるとOpenAIのLeanファイル2,924個・約49万行につながっていた。照合用の問題文は1行で、ゼータ関数は数学ライブラリ Mathlib の定義そのものだった。

照合の条件で、公式の手順と違う点が2つある。comparator が前提にしている隔離の部品 landrun はLinux専用なので、Macでは「隔離をせずにそのまま実行する」代わりのものに差し替えた（照合の中身は同じだが、隔離の保証はない）。また、素数定理などの外部ライブラリには、OpenAIの互換パッチ（Lean 4.34.1向け）をそのまま当てている。

合格でも「問題の全部」とは限らない

Leanが保証するのは、書かれた問題文に対して証明が正しいところまでだ。その照合用の問題文を書いたのもOpenAIで、有名な問題と同じ意味かは人が確かめる必要がある。OpenAIのLeanの説明ファイルを読むと、範囲が一部分だけのものもあった。ヒルベルト第16問題のLeanは「5次のリエナール系では極限閉軌道は最大2個」という特別な場合だけで、上限の存在そのものは紙の証明だ。アンダーソン局在のLeanは「スペクトルが区間になる」という補助の主張で、本体の「局在」は入っていない。

また、372件の全部が初めての手柄ではない。ナイマルクの問題は、2週間前の9月22日に田中氏がZFCでの反例をarXivに出していた（arXiv 2609.26930）。クルーゼ予想の基本形は、7月27日にShanmu Jin氏がGPT-5.6 Solの支援で証明を出したとWikipediaにあり、OpenAIの結果はより強い版にあたる。

数学者はどう見ているか

Scientific Americanは、MITのAndrew Sutherland氏の次の言葉を伝えている。

Until and unless they release the model and people can replicate their results, I think you should treat any claims about one-shotting problems with a single agent as unverified. We should ask for receipts.

（モデルが公開されて結果を再現できるまでは、1つのエージェントで一発で解いたという主張は未検証として扱うべきだと思う。領収書を求めよう）

トロント大学のDaniel Litt氏はこう述べている。

If we want to know the answers to these math questions, I see no reason why we should ask the company to keep them secret from us. To me, it's going to be a good thing for mathematics.

（この問題の答えを知りたいなら、会社にそれを秘密にさせる理由はない。私には、数学にとって良いことに思える）

同誌によると、独立した顧問団はモデル・正確なプロンプト・計算時間の公開を勧めていたが、OpenAIが出したのは平均の計算時間などの統計で、プロンプトは推論の要約10件に抜粋が載っているだけだ。OpenAIの広報は、社内の数学者もまだ多くを理解していないと述べ、同誌は読み解くのに数か月かかるとしている。

この記事で確かめきれなかったこと

• 372件はすべてOpenAIの主張で、人間による査読はまだ。
• 自由群因子・キャノン予想・カプランスキーの零因子予想・マーラー予想などは、出された年を一次資料で確かめられなかったので年を書いていない。
• 論文の日付は論文に書かれた日付で、証明を見つけた日とは限らない。
• arXivとの比較（世界の数学の1か月分の1割近く）は、arXivの9月分とOpenAIの9月10日〜10月6日分の比較で、期間は完全には重ならない。
• 段の分け方は筆者の判断。照合の結果は「書かれた問題文に対して証明が正しい」ことの確認で、問題文が有名な問題と同じ意味かの確認ではない。