OpenAIは2026年10月6日、未公開の社内AIモデルが生み出した数学研究の成果を、722本の原稿と証明資料としてGitHubで公開した。関連する論文をまとめた372の成果グループには、リーマン予想に関わる零点の研究や、円周率πの性質を扱った原稿も含まれる。
9月には「100件を超える未解決問題を解いた」と主張していた同社が、個々の結論や検証資料を外部から確認できる形で公開したことで、数学者が内容を検証するための材料は増えた。ただし、原稿を公開することと、その証明を人間が理解し、次の研究に活用できるようにすることの間には、なお大きな隔たりがある。
722本の原稿と372の成果グループは何を数えているのか
公開されたopenai/mathには、論文PDFに加え、成果の概要や、一部の証明を機械的に検証するための資料が収められている。
722という数字は、公開された個別原稿の本数を表す。一方、372の成果グループは、中心となる結論とその補足的な論証、そこから導かれる結果や別証明などをまとめた区分である。「722件の独立した未解決問題を解いた」という意味ではない。
OpenAIは、既存の数学ベンチマークではモデルの性能差を測りにくくなったため、未解決の研究問題を使った評価を拡大したと説明している。モデルには約4,000問を提示し、その出力を関連する成果ごとに整理したうえで、一定の重要性があるものを今回の原稿群としてまとめた。
したがって、約4,000という問題数、372という成果グループ数、722という原稿数はそれぞれ異なる単位である。722や372を4,000で割って、モデルの「正答率」や「問題解決率」を求めることはできない。
計算量についても注意が必要だ。同社によると、大半の結果は共通の手順で得られ、1件あたりの平均計算量は、その社内モデルを使ってChatGPT Proで約3時間思考させる場合に相当するという。
これはあくまで計算量を換算した表現であり、すべての問題が実時間で3時間以内に解けたという測定結果ではない。一般向けのChatGPTに同じ問題を入力すれば、同じ結果を再現できるという保証でもない。
さらに、ゼータ関数の零点が存在しない領域に関する研究と、複素乗法を持つアーベル多様体についてのホッジ予想は、この共通手順の例外とされている。実部が11/12を超える領域を扱った原稿には、読みやすくするために人間が編集したものもある。
したがって、平均的な計算量だけから、個々の成果にどれだけの作業が必要だったのか、人間がどの程度関与したのかまで一律に推測することはできない。
今回公開されたのは、OpenAIを著者として掲げるプレプリント群である。全体が査読を通過した研究成果として公開されたわけではなく、同社自身も、形式化されていない結果の一部には問題が含まれる可能性があると認めている。
リーマン予想、π、ホッジ予想で何を主張しているのか
「準リーマン予想」と題する9月30日付の原稿は、リーマンゼータ関数を含むすべてのディリクレL関数について、複素変数の実部が7/8を超える半平面には零点が存在しないと主張している。
零点とは、関数の値がゼロになる点のことだ。リーマンゼータ関数の零点がどこに存在するかは、素数の分布の規則性と深く関係している。
ここで重要なのが、7/8という境界である。リーマン予想そのものが主張するのは、非自明な零点がすべて実部1/2の直線上に存在するということだ。
実部7/8より右側に零点がないことを証明できても、1/2と7/8の間に零点が存在する可能性までは排除できない。今回の原稿が正しければ重要な前進となるが、リーマン予想そのものを解決したことにはならない。
より身近な数を扱った例が、「πの無理数度は2」と題する9月24日付の原稿だ。
無理数度は、ある無理数を分数でどれほど精密に近似できるかを表す指数である。πを22/7や355/113のような分数で近似するとき、分母を大きくしながら、どこまで極端に精度の高い近似を続けられるかに関わる。
原稿の主張を具体的に表すと、任意の正のεに対し、分母qが十分大きければ、どの整数pを選んでも近似誤差はqの「−2−ε乗」以上になるというものだ。つまり、分母の大きさに比べて極端に精密な近似が無限に続く可能性を制限する結果である。
ただし、「十分大きい」とされる分母の境界を具体的に計算できるとはしておらず、すべての分数に共通する一定の定数を使って誤差の下限を与える主張でもない。
もう一つの9月30日付原稿は、複素乗法（CM）を持つ複素アーベル多様体について、有理ホッジ予想を証明したと主張している。
ホッジ予想は、大まかに言えば、幾何学的な空間に現れる特定の構造を、代数方程式で記述される部分から表現できるかを問う問題である。原稿は、CMを持つアーベル多様体では任意の次元で成り立つとしているが、対象はあくまで「CMを持つアーベル多様体」に限定される。一般の対象を含むホッジ予想全体の解決とみなすことはできない。
著名な未解決問題の名前が並ぶほど、問題名だけでなく、実際に何を証明したと主張しているのか、その対象と条件を確認する必要がある。
これらの原稿は、今後専門家が検証していく対象であり、問題名だけを取り出して「解決済みの未解決問題一覧」とみなす段階にはない。
Leanで確認できる範囲と、162本という数字
2026年10月7日に確認した形式化目録には、主結果が形式化された原稿として162件が登録されている。
これは公開された722本の原稿の22.4%に当たる。割合は、形式化目録に掲載された162件をREADMEに記載された722本で割り、100を掛けて小数第1位に丸めたものだ。
ただし、22.4%という数字は、主結果の形式化資料が目録に登録されている原稿の割合を示すにすぎない。各原稿の全文が形式化された割合でも、独立した第三者による検証が完了した割合でもない。
同じ目録には185件の主要定理が記載されているが、一つの原稿に複数の定理が含まれる場合があるため、原稿数と定理数が一致する必要はない。目録のレビュー状態も「未確認」とされており、形式化資料が存在することを査読完了とみなすことはできない。
Leanは、定義や前提を明示した定理について、証明の各段階が論理規則に従っているかをコンピューターで確認するための言語・定理証明支援系である。文章では見落としやすい論理の飛躍を、機械が検証できる形に置き換えられる。
今回の資料にはさらに、あらかじめ用意された課題と提出された形式証明を照合するComparatorの設定も含まれている。
Comparatorが所定の条件で確認するのは、提出された解答が課題と同じ定理を証明していること、許可された公理だけを使用していること、そしてLeanの検証中核であるカーネルが証明を受理することだ。
単に「何らかのLeanコードが実行できた」ことを確認するだけでなく、何を証明したのかまで明確にしたうえで検証できる。
ただし、形式化されている範囲は個々の定理ごとに確認する必要がある。
例えば今回の準リーマン予想用の設定では、リーマンゼータ関数について、実部7/8より右側ではゼロにならないという定理が指定されている。
この設定が存在するからといって、原稿が扱うすべてのL関数や、論文中のすべての説明まで独立に形式検証されたと結論づけることはできない。
さらに、形式化された課題と解答が正しく対応していても、その課題自体が元の数学的問題を正確に表現しているかどうかは、別途確認する必要がある。
証明が既存研究に何を加えたのか、そこで使われた発想を別の問題へ応用できるのかといった点も、形式証明がカーネルを通過しただけでは分からない。機械による論理検証と、専門家による数学的な理解には、それぞれ異なる役割がある。
数学界の公開指針と、今回のGitHub公開
数学とAIについて議論する独立諮問グループAGMAIは、数学コミュニティから600件を超える回答を集め、9月29日にAI生成数学の公開指針を発表した。OpenAIは、今回の公開方法にその助言を取り入れたと説明している。
指針と10月6日のOpenAIの発表を照らし合わせると、すでに実施された対応と、今後の課題を分けて確認できる。
| 比較する項目 | AGMAIの9月29日指針 | OpenAIの10月6日公開内容 |
|---|---|---|
| 保管と改訂 | AI研究室が管理しない学術的な保管先、永続的な引用識別子、変更履歴を用意する | OpenAIのGitHubで公開。原稿ごとの引用情報と旧版を残す改訂方針を示し、コミュニティによる代替保管先を検討中 |
| 生成過程の開示 | 各成果について、モデル名やプロンプト、推論要約、時間、計算費用の見積もりを示す | 未公開の社内モデルを使用したと説明。推論要約10件、平均計算量、約4,000問という試行数を公開 |
| 形式化 | 可能な限り証明を形式化し、目録と比較検証用の課題を添える | Lean資料と目録、Comparator用の設定を公開。形式化は一部の原稿に限られ、今後追加予定 |
| 人間による理解 | 内容の理解を進める活動に資金を提供し、支援先の決定は既存の非営利機関に委ねる | 成果を理解するためのワークショップ、会議、特別プログラムへの資金支援を表明。詳細は今後公表 |
この表は、AGMAIの指針の4項目と、OpenAIの発表やREADMEに明記された内容を対応させたものであり、722本すべてが指針に準拠しているかを判定したものではない。
OpenAIは改訂履歴や形式検証の資料を公開したが、成果を生み出したモデルへのアクセスや、OpenAIから独立した保管場所の整備は今後の課題として残る。
成果を誰でも追跡できることと、数学者自身が同じ研究ツールを利用できることは別である。
AGMAIの指針はそもそも、広い研究コミュニティが利用できない専有モデルを使って高度な数学の未解決問題を大量に解かせる取り組みを支持しておらず、その中止を求めている。
一方で、生み出された成果については速やかな公開を求める。そのうえで、内容を理解するために必要な負担を、公開後の数学者だけに押し付けないようAI研究機関側にも求めている。
公開当日の10月6日の声明でも、同グループは今回の出来事を数学にとって重大なものと位置づける一方、OpenAIへ助言した事実は、公開された成果の影響を評価したことや、OpenAIが成果を生み出した方法を支持したことを意味しないと明記している。
AGMAIは企業から独立して活動しており、数学界全体を代表する組織でもない。OpenAIがAGMAIと協議したという事実を、数学者による成果の認定と受け取るのは適切ではない。
公開された証明を、次の研究へつなげられるか
OpenAIは成果の理解を支援する会議などへの資金提供を約束し、成果を生み出したモデルについても、責任ある形で公開できるよう取り組んでいると説明している。
ただし、今回の発表ではモデルの提供時期や利用条件は示されておらず、資金支援の具体的な仕組みもこれから明らかになる。
AGMAIが示した懸念の一つは、将来の数学研究が「AI企業が出した結果を人間が理解する作業」に偏ってはならないという点にある。
数学者自身が問いを立て、独自の手法を発展させ、企業がAIの能力を示すために選ばなかった研究テーマについても自由に探究できる必要がある。そのための条件として、AGMAIは高性能な研究ツールや十分な計算資源へ公平にアクセスできる環境を挙げている。
これは、証明を受け取る側の研究者にも、次の研究テーマを決める主導権があるかという問題でもある。
完成した原稿を読めるようになっても、そこから生まれた新しい疑問を同程度の能力を持つモデルで試せなければ、研究できる方向には偏りが残る可能性がある。論文を公開することと、その成果を起点に新たな研究を進められる環境を整えることは、密接に関係しているが同じではない。
今後の焦点は、専門家が個々の証明を検証し、その発想を分かりやすく説明し、別の問題へどのように応用できるかを明らかにできるかどうかだ。
さらに、モデルへのアクセスや研究支援が、OpenAI自身が選んだテーマ以外を研究する人にも広がるのかも重要になる。
そこまで進めば、今回の大量公開は単なるAIの成果一覧ではなく、数学者が自らの問いを出発点として新たな研究を進めるための知識と道具へとつながっていく。
