OpenAIの数学論文719本：助言グループの指針とのずれと、Lean検証の限界

OpenAIは2026年10月6日、社内のモデルが書いた数学の論文を、GitHubのリポジトリopenai/mathでまとめて公開しました。Xの投稿では、プリンストン高等研究所（IAS）の数学者の助言グループに相談し、その助言を取り入れたと書いています。ところが2日後、TechCrunchは「OpenAIの数学の解答は、まだ分野の基準を満たしていない」と報じました。

この記事では、公開されたものの中身を確かめた上で、助言グループの指針と今回の公開を項目ごとに比べます。あわせて、「Leanで検証済み」の証明に残る問題を、論文と一次資料で確かめます。

公開されたもの#

READMEによると、公開されたのは、未公開の社内モデルが書いた論文と、それを支える証明の資料です。OpenAIは、既存の数学の評価で成績が頭打ちになったため、未解決の研究課題での評価を広げたと説明しています。

論文は719本で、関連する論文を372の系統（family）にまとめています。系統は、主な結果と、その補助の議論や別証明をまとめたものです。モデルに出した問題は約4,000問でした。結果1件あたりの計算量は、ChatGPT Proの思考時間に換算すると平均3時間分に当たります。ほとんどの結果は同じ手順で出したもので、例外はリーマンゼータ関数が零点を持たない領域の研究と、CMアーベル多様体のホッジ予想の証明です。前者の一部は、人が読みやすく書き直しました。

モデルの推論の要約は、10の系統の分だけが公開されました。Leanで形式化したのは、主要な結果のうち300本（約42%）です。

公開直後の報道では論文は722本でした。更新履歴によると、OpenAIは10月7日、符号の誤りで議論が成り立たなくなった1本と、その構成に頼っていた2本、合わせて3本を取り下げました。ほかに14本で証明や主張、古い引用を直し、13本で引用先を新しい版に更新しています。READMEも、形式化していない結果には問題があるかもしれないと認めています。

AGMAIの指針が求めたこと#

助言グループは「数学と人工知能に関する助言グループ（AGMAI）」で、IASが受け入れています。AGMAIのサイトによると、OpenAIが外部の諮問委員会を作ろうと一部の数学者に声をかけたのがきっかけで、話し合いの結果、どのAI企業からも独立したグループになりました。メンバーは9人で、報酬は受け取りません。AI企業の決定に関わる権限はなく、決定の責任はその企業にあると書いています。

AGMAIは9月29日、600件を超える数学者のアンケートをもとに、AIが生み出した数学を公開するときの指針を出しました。冒頭で、外部から使えない独自のモデルで高度な数学の問題を試すのをやめるよう求め、この慣行を支持しないと明言しています。人が理解していない論文を公開する場合の柱は、結果ごとの情報の公開、形式化、公開先、人が理解するための活動への資金の支援です。次の節の表で、今回の公開内容と比べます。

指針と今回の公開の比較#

READMEと報道から分かる範囲で、指針と今回の公開を並べます。

指針の求め	今回の公開
独自のモデルで試さない	未公開の社内モデルで試したとREADMEに書いている
結果ごとにモデル名、プロンプト、思考の過程の要約を出す	要約は10の系統の分だけ
時間と計算費用を出す	ChatGPT Proの思考時間に換算した平均3時間という全体の数字だけ
できる限り形式化する	主要な結果の約42%
自然言語と形式化の対応を機械で読める形で示す（あると役立つという書き方）	TechCrunchによると、出していない
解けなかった問題の数と、問題の選び方を出す	出した問題が約4,000問という数だけ。解けなかった数と問題の選び方は書いていない。載せる結果は、一定の意義があるものに絞ったという説明がある
AI企業が管理しないリポジトリに置く	OpenAIのGitHubに置いた。コミュニティが管理する置き場を検討中とREADMEに書いている
結果の重要さと複雑さに応じて、人の理解を進める活動を資金面で支える（例として研究集会、長期の研究グループ、ポスドクや学生への資金）。支える先はAI企業ではなく既存の非営利団体が決める	OpenAIのブログで、研究集会や特別なプログラムに資金を出すとし、詳細は近く公表するとしている

満たした点もあり、TechCrunchは、結果をできるだけ早く出すことや、モデルが結論に至った過程の情報を付けることは守ったと書いています。取り下げや修正を版として残す方針も、指針の求めに沿ったものです。

AGMAIは公開と同じ10月6日に声明を出しました。助言したことは、結果の重要性を判断したことでも、OpenAIが結果を得た方法を認めたことでもないとしています。指針がどこまで守られたかを評価するのは数学界だという立場で、TechCrunchがより詳しい評価を求めても、回答はありませんでした。

Leanで検証済みでも残る問題#

形式化した証明にも問題が残ることを示したのが、ケンブリッジ大学とキングス・カレッジ・ロンドンの研究者3人が10月6日に出した論文です。対象は、OpenAIが9月に発表したNavier–Stokes方程式の解の爆発（有限時間で解が発散すること）の証明です。

論文が扱うのは自動形式化と呼ばれる工程です。AIが自然言語で書いた証明を、AIが定理証明支援系のLeanのコードに訳します。Leanのコードがエラーなく通れば、そのコードが表す定理は正しいと機械で確かめられます。しかし、訳が元の証明の意味を正しく写しているかどうかは、Leanでは確かめられません。

論文はOpenAIの証明でこのずれが実際に起きていることを示しました。例えば論文の補題8.6の式(8.19)は、出力の微分をm+4階までの入力の微分で抑えると書いています。対応するLeanのコードは、m+5階の微分を条件に使っていて、論文より弱い主張しか証明していません。論文の著者は同じずれがLeanのコードの各所にあると書き、具体例を2つ挙げています。

著者は、OpenAIの自然言語の証明が誤りだとは言っていません。言っているのは、Leanでの検証が通っても自然言語の証明が正しい保証にはならないということです。結論では、OpenAIの証明もほかの自動で形式化した証明も、ほかの証明と同じ査読を経るまでは、そのまま信用すべきではないとしています。同時に発表されたEuler方程式の証明にも同じずれがある可能性が非常に高いと見ていますが、こちらはまだ示していません。

指針は自然言語と形式化の対応を機械で読める形で示すと役立つとしています。対応が示されていれば、このずれを見つけやすくなりますが、今回の公開には含まれていません。

Navier–Stokes方程式の証明には、別の経緯もあります。同じ問題にはニューヨーク大学のTristan Buckmasterも取り組んでいました。TechCrunchの9月の記事によると、Buckmasterは、自分たちの進み具合がOpenAIに伝わったあとで、OpenAIが取り組みを始めたと主張しました。OpenAIは彼らの研究を公開前に見たことはないと説明しています。

数学者が問題にしていること#

AGMAIの指針の背景にあるのは、論文の著者は内容を理解し、正しさを自分で確かめ、責任を持つという数学の慣行です。大きな成果を出した数学者は、各地のセミナーや学会で説明し、質問に答えます。指針は、人が理解しないまま大量の結果を公開するなら、理解が後から追いつくようにする責任はAI企業にあるとしています。

Terence Taoは、公開と同じ日にMathstodonへの投稿で、この点を指摘しました。OpenAIの名前は挙げていません。投稿によると、AIに問題を解かせる人は、目的の問題が解けると分野そのものへの関心を失いがちで、結果について質問に答えたり講演したりできるほど出力を理解していません。その結果、従来の大きな成果に比べて、セミナーや共同研究が生まれず、分野に加わる人も増えないと書いています。一度解かれた問題は未解決には戻らないので、問題が大量に刈り取られると、分野そのものがやせていくという見方です。

ハーバード大学のMelanie Woodは、AGMAIのメンバーでもあります。TechCrunchに対し、モデルが出した解答は公開の時点では人に理解されておらず、仕事はそこから始まると話しています。

まだ分からないことと、今後見る点#

719本のうち、人が理解して責任を持てる論文がどれだけあるかは、まだ分かりません。公開の翌日には3本が取り下げられ、14本が修正されていて、査読の前の時点でも誤りが見つかっています。

指針に近づいたかを見る手がかりは3つあります。形式化の割合が上がるか、自然言語と形式化の対応表が出るか、論文がコミュニティの管理する置き場に移るかです。