数学者団体のAssociation for Human Mathematics（AHM）は2026年10月7日、OpenAIとの協力を中止するよう数学者に呼びかける声明を発表した。前日にOpenAIが700本を超えるAI生成の数学論文の原稿を一斉公開したことについて、研究の信頼性や人間による理解を軽視していると批判した。一方、OpenAIが9月に発表したナビエ–ストークス方程式の解法をめぐっても、自然言語で書かれた証明と、機械検証用のLeanコードに食い違いがあると指摘する論文が登場している。AIが数学の難問に対する証明を生成できるようになるなか、その正しさを検証し、内容を理解して次の研究につなげる仕事を誰が担うべきなのか。数学界では、研究の進め方そのものをめぐる議論が広がっている。
OpenAIとの協力停止を求めるAHM、対話を続けるAGMAI
AHMは10月7日の声明で、OpenAIが700本以上の数学論文の原稿を一度に公開した行為について、学術的な成果を示すものというよりも、企業の力を誇示する行為だと批判した。
声明では、数学者が求めていない研究をAI企業が独自に進め、人間による理解を重視してきた数学研究の慣行を無視したと指摘。数学者に対してOpenAIとの協力を中止し、人間の理解を中心に据えた研究へ立ち返るよう呼びかけている。
ただし、今回の声明はAHMの広報ワーキンググループが発表したものであり、数学界全体で合意された決議ではない。
また、声明が掲載されたのは、フィールズ賞受賞者である数学者Terence Tao（テレンス・タオ）氏のブログだが、冒頭にはAHMによるゲスト投稿であることが明記されている。
したがって、この協力停止要求をTao氏個人の声明と捉えるのは適切ではない。
一方、OpenAIとの対話を続けながら、研究成果の公開方法を改善しようとしている数学者もいる。
その中心となっているのが、米Institute for Advanced Study（IAS）を拠点とするAdvisory Group on Mathematics and Artificial Intelligence（AGMAI）だ。
AGMAIの公式説明によると、同グループは9人の研究者で構成され、AI企業から独立して活動している。メンバーはこの助言活動についてAI企業から報酬を受け取っておらず、企業の意思決定に関与する権限も持たない。
10月6日に公開した声明でも、OpenAIへ助言していることを、同社の研究手法や成果を承認したと受け取るべきではないと強調した。
その一方で、OpenAIとの議論は建設的だったと評価し、ほかのAI企業とも対話を続ける姿勢を示している。
AHMとAGMAIの大きな違いは、AI企業との関わり方にある。
AHMはOpenAIとの協力停止を求めているのに対し、AGMAIは対話を通じて、AIが生み出した研究成果の公開方法や、その後の研究環境を改善しようとしている。
ただし、両者の問題意識には共通する部分もある。
AGMAIが9月29日に発表した指針では、一般の研究者が利用できない独自モデルを使って、AI企業が高度な数学の問題を解く実験を続けることに明確に反対し、その中止を求めている。
一方、すでに得られた重要な成果については、責任ある方法で速やかに公開するとともに、数学者による理解を深めるための活動を支援すべきだとしている。
OpenAIは10月6日の発表で、今後も社内の高性能モデルを数学や科学の問題で評価していく方針を示した。
同社は、こうした研究を通じてモデルの能力を高め、将来的に研究者へ高度なAIツールを提供したいと説明している。
しかし現時点では、今回の数学的成果を生み出したモデルを一般の研究者が利用することはできない。
AIが生成した論文を公開することと、数学者自身が同じツールを使い、自分の研究課題に取り組めるようにすることは別の問題だ。
この点について、OpenAIと数学者の間には依然として意見の隔たりが残っている。
700本以上の数学論文を公開、翌日には3本撤回
OpenAIが公開した数学論文の原稿については、すでに誤りの発見と修正が行われている。
同社のGitHubリポジトリにある10月7日付の更新履歴によると、分裂アーベル多様体に関するWeil類の代数性を扱った原稿で、数式の符号に誤りが見つかった。
この誤りにより、証明の中で必要とされていた項の相殺が成立しなくなり、論証の一部が無効となった。
さらに、この結果を利用していたKuga–Satake対応やK3曲面の積に関する別の原稿にも影響が及んだため、OpenAIは計3本を撤回した。
このほか、14本の原稿についても、証明の修正や定理の主張、前提条件の明確化などを行っている。
一つの証明に誤りが見つかると、その結果を利用する別の証明にも影響が及ぶ。今回の撤回は、数学研究におけるこうした依存関係の重要性を示している。
ただし、3本が撤回されたからといって、残りの原稿にも同じ割合で誤りが含まれていると推定することはできない。逆に、撤回されていない原稿がすべて正しいと確認されたわけでもない。
10月9日時点の公開リポジトリでは、719本の原稿が372の研究系列に分類されている。
研究系列とは、中心となる研究成果に加え、それを補足する論証や別の証明、関連する結論などをまとめた単位だ。
したがって、719本という原稿数を、そのまま719件の独立した未解決問題を解決した数として扱うことはできない。
また、OpenAIは一部の証明をLeanという証明支援システムで形式化し、機械的に検証できる資料も公開している。
10月7日の更新履歴では、形式化の進捗について「300 / 719 = 約42%」という数字が示された。
ただし、この数字は公開中の原稿数719本を分母とした進捗指標であり、372の研究系列に対する割合ではない。また、原稿のすべての記述や論証が形式化され、検証を終えたという意味でもない。
機械検証用の資料が存在することと、専門家がその内容を理解し、査読によって正しさを確認することは別である。
さらにOpenAIによると、今回の評価では社内モデルに約4,000問が与えられ、得られた成果の大部分は、平均でChatGPT Proの約3時間の推論に相当する計算量を使って生成されたという。
ここでいう3時間は計算量を表す指標であり、すべての問題が実時間で3時間以内に解けたことを意味しない。
また、モデルに与えた問題の数、研究系列の数、原稿の数は、それぞれ異なるものだ。
これらの数字だけでは、AIが未解決問題を解く成功率や、人間の研究者と比べた解決速度を正確に算出することはできない。
Leanで証明が検証されても、元の論文が正しいとは限らない
AIによる数学研究では、証明を機械的に検証できることが重要な成果として注目されている。
しかし、Leanが証明を受理したからといって、自然言語で書かれた元の論文まで正しいと保証されるわけではない。
この問題を具体的に指摘したのが、Alexander Bastounis氏、Fabian Circelli氏、Anders C. Hansen氏による研究だ。
3氏は10月6日、「Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs」と題する論文をarXivに投稿した。
これは査読前のプレプリントであり、自然言語で書かれた数学的な証明をLeanのコードに変換する「自動形式化」の問題を検討したものだ。
Leanは、数学の定理や仮定、証明の手順を厳密な形式で記述し、論理的に正しいかどうかをコンピューターで検査するための証明支援システムである。
ただし、Leanが検証するのは、あくまでコードとして記述された定理と証明だ。
自然言語の文章をAIがLeanに変換する過程で、定理の意味や前提条件が変わってしまえば、元の論文とは異なる内容を機械的に検証している可能性がある。
今回の論文が取り上げたのは、OpenAIが9月8日に解法を発表したナビエ–ストークス方程式の問題だ。
OpenAIは、流体の運動を記述するナビエ–ストークス方程式について、有限時間で解が特異性を持つことを示す証明が得られたと主張し、自然言語による論文とLeanで形式化した証明を公開していた。
Bastounis氏らは、この自然言語の論文と特定のバージョンのLeanコードを比較し、両者の内容が一致していない部分を指摘した。
例えば、論文の第3.1節では、ある数学的な評価式について、自然言語の証明では入力関数に最大で「m+4階」の微分可能性を求めているのに対し、対応するLeanコードでは「m+5階」が必要になっていると指摘している。
これは、Lean側の証明では、元の論文よりも一段厳しい条件を使っていることを意味する。
そのため、Leanコードで証明が成立していても、自然言語の論文に書かれた、より強い主張がそのまま検証されたことにはならないという。
さらに第3.2節では、圧力に関する評価についても、元の論文とLeanコードで証明の手順や内容が一致していないと指摘した。
ただし、著者らは、OpenAIが公開した自然言語の証明そのものが正しいかどうかは判断していないと明記している。
また、今回の検証は特定のバージョンのLeanコードを対象としたものであり、OpenAIが10月6日に公開した大量の数学原稿すべてを調査したものではない。
指摘されたのは、Leanによる形式的な検証と、自然言語による証明との対応関係が十分に保証されていないという問題だ。
したがって、この不一致だけを根拠に、OpenAIが主張するナビエ–ストークス方程式の解法が誤りだと結論づけることはできない。
一方で、機械が受理したという事実だけで、元の論文の正しさまで保証されたと考えることもできない。
数学の証明を検証するには、三つの異なる確認が必要
今回の研究が示しているのは、機械的に検証できる証明と、人間が理解できる数学的な説明の間には、まだ確認すべき段階があるということだ。
特に、AIが生成した数学的成果を研究に利用するには、大きく三つの点を確認する必要がある。
| 確認する対象 | 確認すべきこと | それだけでは分からないこと |
|---|---|---|
| 形式化された証明の論理 | 記述された定理が、明示された仮定から論理的に導かれるか | 元の論文と同じ内容を証明しているか、人間が理解できるか |
| 自然言語と形式化の対応 | 定義や前提条件、証明の内容が変換後も正しく保たれているか | 証明の考え方を理解し、ほかの問題に応用できるか |
| 人間による理解 | 専門家が証明を説明し、質問に答え、次の研究に活用できるか | 形式的な論理の検証を省略できるわけではない |
この分類は、Bastounis氏らの検証論文とAGMAIの9月29日の指針を基に、数学的成果を評価する際の確認事項を整理したものだ。個々の論文の正しさを判定するものではない。
まず、Leanなどの証明支援システムを使えば、形式的に記述された定理が、与えられた仮定から論理的に導かれるかどうかを厳密に検査できる。
ただし、そのためには、証明に未解決の部分が残されていないことや、想定外の公理や仮定に依存していないことも確認しなければならない。
次に、形式化された定理と証明が、自然言語の論文で主張されている内容と一致しているかを確かめる必要がある。
仮定が一つ追加されていたり、定理の主張が弱くなっていたりすれば、機械検証が成功しても、元の論文の結論を裏づけることにはならない。
さらに、その証明が何を意味し、どのような新しい考え方を含んでいるのかを理解することも重要だ。
数学では、新しい定理が証明されると、その論証をほかの研究者が読み解き、より簡潔な説明や一般化、新たな応用方法を見つけていく。
証明が正しいという事実だけでなく、そこで生まれた考え方を共有できるようにすることも、研究の発展には欠かせない。
こうした理解の難しさは、すでに専門家の間でも問題になっている。
計算量理論の研究者Scott Aaronson氏は、10月7日のブログで、長年Unique Games Conjecture（ユニークゲーム予想）を研究してきた妻のDana Moshkovitz氏から受け取ったメッセージを紹介した。
Moshkovitz氏は、OpenAIが公開した関連論文について、説明が分かりにくく、先行研究の引用にも疑問があり、AIの助けを借りなければ読み進めることが難しいと述べている。
これは証明の正しさを最終的に判断した報告ではなく、専門家が内容を理解しようとしている段階での反応だ。
AIが高度な証明を生成できても、その内容を専門家が読み解き、数学的な意味を明らかにするまでには、相応の時間と労力が必要になることを示している。
数学の価値は、難問を解くことだけではない
AIによる数学研究をめぐる議論は、単に証明の正しさを確認する方法だけにとどまらない。
数学研究で何を成果とみなし、どのような活動を評価すべきなのかという、より根本的な問題にも及んでいる。
9月11日には、Tao氏を含む25人のフィールズ賞受賞者が、AIによる数学研究の進め方に懸念を示す共同声明を発表した。
声明では、数学の難問を解くことは、数学的な概念や構造を深く理解し、新しい洞察を得るための手段だと指摘している。
これまで数学では、長年の未解決問題に対する証明が発見されると、その内容を研究者同士で議論し、説明を整理し、より簡潔な証明や新しい研究方法を見つけてきた。
さらに、その成果が教科書などにまとめられ、次の世代の研究者が学び、別の問題に応用できるようになるまでには、長い時間をかけた研究の積み重ねがある。
難問が解決されたという結果だけでなく、その過程で得られた考え方を理解し、共有することも数学の重要な営みだという。
Tao氏も10月6日の投稿で、AIによる数学研究が進むことで、従来の研究活動のあり方が変わる可能性に言及した。
例えば、AIを使って難問の証明を得た人が、その数学分野に深い関心を持っていなかったり、証明についての質問に答えられなかったりする場合、従来の研究では自然に生まれていた講演や議論、共同研究が十分に行われなくなる可能性がある。
同氏は、こうした新しい研究環境を「Math 2.0」と位置づけ、最初に問題を解決したことだけを高く評価する従来の仕組みを見直す必要があると提案している。
証明の内容を分かりやすく説明することや、研究者同士の交流を促すこと、そこから新しい研究の方向性を見つけることにも、より大きな価値を認めるべきだという考え方だ。
Tao氏は、AIがこうした活動を支援する可能性も認めている。
つまり、問題になっているのはAIを数学研究に使うこと自体ではなく、証明を生成する速度だけが重視され、その成果を理解して発展させる仕事が軽視されることだ。
この問題を、AIに仕事を奪われることへの数学者の反発と捉えるだけでは、本質を見落とす。
高度な数学的成果を理解し、誤りを検証し、分かりやすい解説や教材を作るには、専門家の時間と研究資金が必要になる。
AI企業が研究課題を選び、大量の証明を公開する一方、その後の検証や理解を数学者に委ねるのであれば、こうした作業を誰が支え、研究上の貢献としてどう評価するのかという問題が生じる。
OpenAIとAnthropic、異なる研究成果の公開方法にも課題
AIが生み出した数学的成果をどのように公開するかについても、企業によって異なる取り組みが見られる。
Aaronson氏は前述のブログ記事で、OpenAIとAnthropicの公開方法を比較している。
OpenAIは、社内モデルが生成した大量の数学原稿をリポジトリで一括公開した。
これにより、誰でも原稿を読めるようになった一方、内容を理解し、誤りを検証し、研究上の価値を判断する仕事は、数学者の側に委ねられることになった。
一方、AnthropicのAIが発見に関与したアルゴリズム研究では、研究者に報酬を支払い、研究内容を理解しやすい形にまとめたうえで公開する方法が採られたという。
この方法であれば、数学者が成果の説明や整理に時間をかけるための支援を受けられる。
しかし、Aaronson氏は、この方法にも問題があると指摘した。
AI企業が説明を担当する数学者を選ぶことになれば、誰が研究成果の理解や発表に関わる機会を得られるかを、企業側が決めることになるためだ。
つまり、OpenAIの一括公開方式には、成果を理解するための負担が研究者側に集中する問題がある。一方、Anthropicの方式には、企業が研究者の選定に大きな影響力を持つという問題が残る。
AI企業が研究資金を提供するだけでは、研究の主導権や公平性をめぐる問題がすべて解決するわけではない。
OpenAIも、こうした懸念に対応する取り組みを発表している。
同社は10月6日の発表で、AIが生み出した重要な数学的成果について理解を深めるため、ワークショップや学会、特別研究プログラムなどに資金を提供する方針を示した。
具体的な支援内容や規模については、今後発表するとしている。
一方、AGMAIの指針では、支援対象の選定をAI企業や同グループ自身が直接行うのではなく、既存の非営利研究機関が独立して判断する仕組みを勧めている。
研究資金を提供する企業が、どの成果を重要とみなすかや、誰が研究を進めるかまで決めてしまうことを避けるためだ。
さらにAGMAIは、数学者が高度なAIモデルや十分な計算資源を公平に利用できる環境を整えるよう求めている。
研究者がAI企業の選んだ問題を検証するだけでなく、自ら研究課題を設定し、独自の方法で数学を発展させられるようにすることが重要だという。
AIによる数学の進歩を、人間の理解につなげられるか
OpenAIが700本以上の数学論文の原稿を公開したことは、AIによる数学研究が新たな段階に入ったことを示している。
しかし、その成果が数学の知識として定着するには、証明の正しさを確認するだけでなく、内容を理解し、ほかの研究へ応用できる形に整理する必要がある。
今回の撤回や修正、自然言語の証明とLeanコードの不一致をめぐる指摘は、その過程が決して簡単ではないことを示した。
また、研究を支える仕組みについても、AI企業と数学者の間で意見が分かれている。
AI企業がどこまで責任を持って成果の検証や説明を支援するのか。提供する研究資金を誰が配分するのか。そして、数学者自身が高度なAIツールを使い、研究課題を自由に選べる環境をどう整えるのか。
今後は、こうした具体的な取り組みが重要になる。
特に注目されるのは、OpenAIが表明した研究支援がどの程度の規模で実施され、誰が支援対象を決定するのかという点だ。
また、現在は一般の研究者が利用できない高性能モデルについて、どのような条件でアクセスが認められるのかも、数学研究のあり方に大きく影響する。
AIが数学の難問を解く能力を高めても、その証明を人間が理解し、新しい知識として共有できなければ、研究成果の価値を十分に生かすことはできない。
これからの数学研究では、AIが証明を生成する能力だけでなく、その成果を検証し、説明し、次の発見へつなげる仕組みをどこまで整えられるかが問われる。
数学者が自ら研究課題を選び、成果を理解するための時間と資源を確保できること。それが、AIによる数学の進歩を、数学界全体の発展につなげるための重要な条件になる。
