数学が工業化される時代：372件の未解決問題に対してOpenAIが証明を公開

OpenAIは2026年10月6日、未公開のAIモデルが未解決の数学研究課題に取り組んで得た372件の数学成果を公開しました。関連する証明や派生結果をまとめたマニュスクリプトの一覧で、一部には証明支援系Leanで形式化した証明も添えられています。[1][2]

今回の発表には、数学者が十分に調べ切れていなかった命題に対して、高性能なAIを使えば網羅的に証明を試みられるという意義が示されたと言えます。証明の方針策定から、検証、結果の整理までを半自動化できれば、これまで一研究者が研究に割ける時間に制約があるために取り残されていた問いが片付けられるようになります。

OpenAIが公表した命題の証明のすべてが数学の方向性を変えるような重要な成果だとは言えないものの、こうした研究の進め方はもはや「数学の工業化」であり、パラダイムの変化に巻き込まれつつある数学コミュニティからは驚愕（もしくは怨嗟）の声が上がっています。最先端のAIモデルを擁する企業から一度に372件という規模の成果が発表されるという事態に際し、その価値と意味について考えてみます。

372件の成果と公開された原稿

OpenAIの公式資料では、関連するマニュスクリプトをまとめた単位を「系列（result family）」と呼び、372系列に整理しています。一つの系列には、中心となる結果、補助的な議論、結論、別証明などが含まれます。[2]

数値は公式README、更新履歴、初期公開案内によります。[2][3][8] この表から単純な正答率は計算できませんが、約4000問の未解決問題に取り組んだというのは驚くべきことに思われます。OpenAIによれば、結果当たりの平均計算量は、当該モデルによるChatGPT Proの思考計算約3時間相当でした。これはモデルの計算量としてはかなり小さい値です（ただしどの程度のエージェント数を動員したかは不明）。[1]

一方で、既に3件の論文が撤回されており、複数の論文で証明の修正が行われています。数学者の中には証明だけでなく本文中の用語の使い方までもが “AI Slop” 的だと主張する人もおり、AIによる証明自動化のクオリティの低さを嘆く声も聞かれます。検証と、撤回・修正の内訳の詳細については後述します。

AIによる数学の自動化の意義

数学の未解決問題には、長年にわたって多くの専門家が取り組んできた予想もあれば、論文中で指摘されたまま十分に調べられていない問いもあります。既存の結果を別の分野へ適用すると解けるものや、証明の大筋は見えていても細部の確認に手間がかかるものも考えられます。研究者は、限られた時間の中で、取り組む問題を選ばなければなりません。そのため、解ける見込みがあっても、ほかの研究課題を優先して残される問いがあります。AIが文献の知識を組み合わせ、候補を繰り返し試し、証明の細部を埋められるなら、そのような命題を確かめる負担を減らせます。

一般論として、AIによる数学の自動化は、「これまで十分に調べられていない問い」や「（アプローチの方向性には見当が付くが）人間が処理するには時間がかかりすぎる問い」に対する道具として活用できます。特に、近年では数学の証明を定式化するLeanという言語・システムが普及してきており、文章としては “AI Slop” 的な表現であっても、機械的に検証可能な形で証明を共有できるようになりつつあります。現に、AIによる推論を補助的に用いて結論を導いている数学の研究は既に多数存在しています。

こうしたAIの使い方は、個々の結果が数学コミュニティに与える影響は限定的だったとしても、調べられる問題が増えること・誰でも再現可能な形で共有されることに意味があります。得られた証明や反例を集積することで、命題の成立条件の理解や、今後の研究で使える知識や方法論が蓄積されます。この積み重ねは従来人間が行ってきたものであり、ここにAIが参加するというだけに過ぎません。AIはこの営みを大きく加速しますが、それこそがAIによる数学の自動化の意義と言えるでしょう。

数学の進展へのAIの寄与

AIの数学への寄与を切り分けると、「未解決問題に証明を与えること」と「汎用的な方法論を提案すること」に大きく分けられると思います。そのような観点で今回のOpenAIの発表を見てみると、まだまだAIの数学力やセンスは発展途上のようにも思われます。全372件のうち、数学の研究方法や方向を大きく変える成果がどれだけあるかは、下記の観点から個別に評価すべきです。多数の証明を得たという事実や主張自体を数学全体へのコントリビューションと見なすのは誤っています。

例えば公式の成果一覧には、カタラン定数の無理性や、円周率$\pi$の無理数度が2であるという主張も含まれています。[4] 無理数度は、有理数による近似の良さの限界を測る量です。これは$\pi$の無理数性からさらに進んだ結果であり、こうした結果の積み重ねが数学的対象そのものへの理解を進めること自体は間違いありません。

Leanによる検証と、撤回・修正の内訳

Leanによる形式化では、命題や証明を機械が厳密に扱える形で記述します。証明を検査することで、書かれた前提から結論が導かれるかを確認できます。長い議論の論理的な整合性を調べるうえで、有効な手段です。確認する対象は、論文の主定理の場合もあれば、証明を支える補助結果の場合もあります。公式の検証用READMEは、補助結果だけを検証する設定を明記しています。[5] 確認すべきなのは、形式的な証明が通ること、形式化された命題が原稿の主張に対応すること、そして人間が議論を理解して使えることです。この三つを区別すると、何が検証されていて、どんな課題が残っているかが見えてきます。

2026年10月10日（日本時間）に公式更新履歴を確認し、原稿単位で再集計しました。確認できた最新の記録は10月7日付です。撤回3原稿に加え、修正14原稿と、それに伴う引用・版情報の更新13原稿が記録されています。[3]

修正された14原稿の内訳は、Lipschitz高さ関数とAshkin–Teller電流に関する4原稿、Kähler最小モデルと豊富性に関する6原稿、tamingとhypersymplectic変形に関する2原稿、非圧縮輸送と有限計算に関する1原稿、Birch–Swinnerton-Dyer型の公式に関する引用修正1原稿です。また、撤回された3原稿は、分裂アーベル8次元多様体のWeil類、K3曲面のKuga–Satake対応、K3曲面の積の有理Hodge予想を扱っていました。[3] 現在の原稿数は、初期公開の722から撤回分を引いた719です。Leanによる主張の形式化は300／719で、全体の約42％となっています。[2][3]

まず事実関係として、27原稿すべてに証明の誤りが見つかったというわけではありません。一つの誤りがそれを前提とする別の論文へ波及したために数が多く見えているというのが実際のところで、依然として数百の論文の結果は有効（査読待ち）の状態です。生成した原稿を個別に確認するだけでなく、原稿同士の依存関係も点検し、修正の影響を追える状態にする必要があります。

半自動で証明を進めることの意味

研究で活用するなら、研究者が問いを整理し、AIが証明や反例の候補を作り、証明支援系や専門家が確かめる進め方が考えられます。得られた結果を既存研究と照らし合わせ、使いやすい形で説明することも研究者の仕事です。

具体的には、手元の予想を小さな命題へ分ける、反例を探す、仮定を変えた場合を調べる、見つかった証明の一部を形式化する、といった作業です。これらの負担が減れば、研究者はより多くの可能性を試し、見込みのある問題を選べます。

一方で、証明候補を作る速度が上がるほど、文献調査、誤りの発見、説明の整理に必要な時間が問題になります。研究全体の生産性を考えるなら、生成にかかった計算量とともに、人間が理解して再利用できる成果へ仕上げる負担も数える必要があります。

大量公開への反発と、検証を誰が担うか

今回の公開には、数学コミュニティの一部から強い反発が出ています。Association for Human Mathematics（AHM）の広報作業部会は10月7日の声明で、700を超えるファイルの一括公開を批判し、数学者にOpenAIとの協力停止を呼びかけました。声明は、人間の理解を中心に据えた数学研究を求めています。[9] この声明はTerence Taoのブログにも寄稿として転載されています。協力停止を求めている主体はAHMの作業部会であり、数学コミュニティ全体やTao個人の声明ではありません。

OpenAIへ助言してきた独立団体AGMAIも、研究者が利用できない独自モデルで高度な数学の問題を試す慣行を支持せず、その停止を求めています。そのうえで、AIの出力を公開する際には、企業側が文献調査と読みやすい証明の整備を行い、人間の理解を深める活動へ資金を提供するよう提言しています。[7]

こうした批判の核心は、成果を生み出す側と、それを読んで確かめる側の負担の偏りです。企業が大量の成果を発表し、専門家が自分の研究時間を削って欠落した説明や誤りを探す構図が続けば、研究の利益とコストが釣り合いません。今回のGitHub上への大量公開は学術誌の正式な査読に回ったということを意味しませんが、公開後の検証を外部の数学者に事実上委ねるという問題は生じます。これはarXivが “AI Slop” 的な投稿の増加に手を焼いている最近の事情と重なります。事実、OpenAIがarXivではなくGitHub上でマニュスクリプトを公開したのも、大量に同時公開できるような信頼できるプラットフォームが他に無かったということも一因と考えられます。

一般に、研究においては訂正や撤回は起こり得ます。成果の公開のあり方を評価するうえでは、その件数に加え、著者側がどこまで確認し、質問に答え、誤りの影響を追跡できるかが重要です。私は、企業には理解可能な説明と検証の体制を用意する責任があり、研究者には自分の時間を使う対象を選ぶ権利があります。検証への参加や協力の見送りもその選択に含まれますが、今回のように一見すると大言壮語な発表がなされるとコミュニティに対する検証コストの押しつけは避けられません。

実際、自身が取り組んでいた課題が今回のリストの中にある研究者からすると食い扶持を奪われたも同然ですから、OpenAIの発表した証明の真偽を調べることの優先度はどうしても上がってしまいます。

OpenAIは、AIが生んだ主要な結果の理解を進めるワークショップや会議への資金提供を表明しています。[1] 今後は、こうした数学や理論物理学コミュニティへの支援が研究者の独立性と研究時間を守り、学生や若手の研究継続に役立つ形で実行されるか、というOpenAIの企業としての社会的責任が問われています。

研究者と学生の研究計画はどう変わるか

大量の証明を一度に公開することは、その問題に取り組んできた研究者の将来にも関わります。数年をかけて研究してきた問題が先に解かれれば、予定していた成果の新規性が失われ、論文や学位研究の構成を変えなければならない場合があります。学位取得や雇用契約に期限がある学生・若手研究者にとって、テーマの変更は、時間や生活にも直結する問題です。

研究の先行競争に、未公開の高性能モデルと大規模な計算資源によって、多数の問題へ短期間に取り組めるという非対称性が加わっています。AGMAIも、非公開モデルを持つAI企業と研究者との間に格差が生じることを懸念し、数学者が自ら問いを立て、自分たちの研究方向を選べる条件を求めています。[6][7]

私は、今後のAIの能力向上を研究計画に織り込み、一つの問題を最初に解くことだけに学位や研究の継続を依存させない構成を考える必要があると思います。中心となる問いを持ちながら、途中で得られる補題、方法の改良、反例、適用条件の整理などにも、独立した研究上の貢献を見出すということです。あくまで過渡的な措置かもしれませんが、数学コミュニティの持続的な発展を目指すのであれば、世界中のAI企業はこうした仕組み作りや優遇策を積極的に提案し、支援していく義務があるように思います。

---

数学、理論物理、理論化学では、成果を確かめる対象も異なります。AIを使ってどの作業を進め、何を自ら検証するかを、研究課題ごとに具体化することが出発点になります。

理論物理や理論化学では、方程式や関係式等の正しい導出に加えて、採用した仮定や近似が調べたい現象に適しているかを確かめる必要があります。AIが導出や計算を加速するほど、その結果をどの条件で信頼できるかを調べる作業を研究計画の中に明確に置く必要があります。

学生の学習やゼミなどでの訓練でも、AIを実際の研究に使う経験と、自分で論証や計算を組み立てる経験の両軸で進めるのが望ましいでしょう。AIが示した結果を再導出する、反例や極限の場合を調べる、別の方法で確かめる、といった作業を通してAIの出力を評価する力を養えます。問いの設定や検証にもAIを使いながら、採用した仮定と結論の関係を自分で説明できることを目標にします。

研究計画の変更を支える責任は、学生だけでなく、指導教員と研究機関にもあります。指導教員は、一つの結果が先に公表された場合の進め方を学生と（事前に）相談し、研究の節目ごとに計画を見直すべきです。学位審査や採用では、成果の新規性に加え、独自の方法、検証、一般化などの貢献を具体的に評価する必要があります。研究機関には、テーマ変更に必要な指導や資金、期限の扱いを検討する仕組みが求められます。

AI企業にも、成果を理解・検証するための資料を整え、その作業を担う研究者を支援する責任があります。AGMAIは、学生やポスドクが参加する研究活動への資金支援と、モデルや計算資源への公平なアクセスを提言しています。[7]研究者がAI企業の出力を検証する仕事だけに従事する状況を避け、自らの問いを追究できる研究時間と環境を確保することも、支援の目的に含めるべきだと考えます。

まとめ

今回のOpenAIの発表は、十分に追究されていなかった問いを調べ、証明候補を試し、確かめた結果を蓄積する作業にAIを活用できる可能性を具現化したものと感じられます。研究者が時間や労力の制約から取りこぼしていた命題に半自動で証明を与えられるなら、数学の研究の進め方が大きく変わります。まだ成果物のクオリティは人間には及びませんが、数学の知識を押し広げる道具としてAIが本格的に寄与できることを示した歴史的な事件と言えるでしょう。

AIによる数学の自動化の価値を測るには、証明の件数に加えて、得られた方法の汎用性や他の研究での応用可能性までを見極めるべきです。多数の命題と証明を確かめる能力の獲得と、新しい数学を生み出す能力の獲得が、今後の数学におけるAI開発の進むべき道のように思われます。

参考資料

1. 1. OpenAI「Sharing AI progress in mathematics」。2026年10月6日の公開説明。
   2. OpenAI公式リポジトリ「openai/math」。系列・原稿の数、試行した問題数、生成手順、検証状態。
   3. OpenAI「History」。2026年10月7日の撤回・修正・形式化追加の記録。
   4. OpenAI「Overview」。公開側による各系列の主張の一覧。カタラン定数は系列005、円周率の無理数度は系列017。
   5. OpenAI「Comparator challenges」。形式的検証の手順と、補助結果だけを対象とする検証の区別。
   6. Advisory Group on Mathematics and Artificial Intelligence（AGMAI）。2026年10月6日の声明。助言の役割と、成果の理解・評価に関する立場。
   7. AGMAI「Responsible Release of AI-Generated Mathematics」。2026年9月29日。文献調査、説明、検証、研究者のアクセスについての提言。
   8. OpenAI Developer Communityの公開案内。初期公開時の722原稿・372系列の記録。
   9. AHM「Statement on OpenAI’s October 6 Release of Mathematical Documents」。2026年10月7日。Association for Human Mathematics広報作業部会の声明。Terence Taoのブログへの寄稿・転載。

作成日：2026年10月10日。参考資料の最終確認日：2026年10月10日（日本時間）。撤回・修正の件数は同日に確認した公式更新履歴に基づきます。