証明があふれる時代の数学 — Terence Taoの「Math 2.0」が問い直す価値

AIが証明を大量生産できるようになったとき、数学が守るべきは「最初に解いた者」の栄誉か、「理解した者」の共同体か。

導入

2026年10月11日、Hacker Newsのトップページに Terence Tao の講演スライド「Math 2.0」のPDFが上がり、563ポイントを集めた。ファイル名には Caltech と 2026 が入っており、表紙には「October 2026」とだけ書かれている。

このスライドは真空の中から出てきたものではない。同じ週に三つの出来事が続いた。10月6日（米国時間）、OpenAI は社内の未公開モデルが生成した数学原稿群を GitHub リポジトリ openai/math として公開し、Hacker News では「Sharing AI progress in mathematics」というタイトルで1,362ポイントを得た（Hacker News 上では10月7日）。同じ日に Tao は Mastodon に4本組のスレッドを投稿し、「Math 2.0 は数学的進歩をより総合的に評価する必要がある」と書いた。この投稿は10月8日に Hacker News で614ポイントを集めた。そして10月8日、Dan Roberts（X アカウント danintheory）が「我々の GitHub math リポジトリ」を更新したとして3本の撤回を告知し、このニュースも381ポイントを得た。

このブログは9月5日にフェルマーの最終定理の形式化を取り上げ、「検証されたが読まれない証明」は知識なのかを問うた。そのときの問いは一本の巨大な証明に関するものだった。今週起きたことは規模が違う。数百本が一度に放出され、その一部は形式検証を経ており、一部は経ておらず、一部は数日で撤回された。Tao のスライドはこの状況を、個々の証明の真偽ではなく、数学という分野の「報酬構造」の問題として組み直している。本稿では、その組み直しが何を主張しているのか、そしてどこが弱いのかを検討する。

現象分析 — 一週間で放出された証明

まず事実関係を整理しておく。出典は OpenAI リポジトリの README と history.md であり、本稿執筆時点（10月18日）に確認した内容である。OpenAI の公式発表ページはアクセスがブロックされ、直接確認できなかった。

README によれば、このリポジトリは「社内の OpenAI モデルが生成した数学原稿と、その証明成果物」を収めており、現在719本の原稿が372の「ファミリー」にまとめられている。生成方法も記されている。結果の大半は未公開の社内モデルで同一の手順に従って得られ、1件あたり平均で ChatGPT Pro の思考（thinking）計算およそ3時間分を使った。評価期間中にモデルへ約4,000問が与えられ、それをファミリーと原稿に集約し、「適切な水準の重要性」を要求して絞り込んだのが現在のカタログだという。例外も明記されている。リーマンゼータ関数の零点非存在領域に関する作業と、CM アーベル多様体に対するホッジ予想の証明はこの固定手順の例外であり、Re(s) > 11/12 の領域に関する原稿は可読性のために人間が編集したという。

検証状態について、README 自身は慎重である。「すべての結果に Lean による形式化が付いているわけではない」「形式化されていない結果の一部には問題があるかもしれない」と書く。history.md の10月7日の項目は、これを具体的に示している。「分裂アーベル8次元多様体上の Weil 類の代数性」の原稿で符号の誤りが見つかり、安定化トレースの相殺論法が崩れた。その構成に依存する2本の原稿とあわせて3本が撤回された。同じ項目で14本が証明の補修と仮定の明確化によって改訂され、13本が改訂版の関連原稿を引用するよう更新された。形式化は6件追加され、「トップラインの結果の形式化率」は300/719、約42%になったという。撤回された3本が Lean で形式化済みの結果だったかどうかは、この文書だけでは確認できない。Hacker News でもまさにその質問が繰り返された。

OpenAI の公開の直前には、もう一つの文脈がある。AGMAI という数学者の助言グループは9月29日、「AI 生成数学の責任ある公開」と題する勧告を出した。600件を超える回答をもとに勧告をまとめたとし、数学共同体で最も重要な規範の一つは「著者が論文の数学的論証を理解し、自ら正しさを検証し、内容に全面的な責任を負うこと」だと書いた。そして、AI ラボが人間の即時的な理解を伴わずに大量の数学的成果を公開するなら、「人間の理解が後に続くよう責任を負うべき」であり、その理解の発展は「共同体主導で有機的でなければならない」と勧告した。冒頭ではそもそも、ラボがプロプライエタリなモデルで高度な数学問題を試す慣行そのものを支持しないと明言している。

Hacker News の反応は大きく割れた。OpenAI 公開のスレッドでは、あるユーザーがこのリストは自分が参照する「上位500の未解決問題」のうち90問を完全に解いたと主張していると集計した（直接の引用ではなく、コメントの要旨の要約）（@zone411）。別のユーザーは、博士課程の途中で似た結果の原稿を半分書いている学生は、これから何をすればいいのかと問うた（直接の引用ではなく、コメントの要旨の要約）（@open592）。さらに別のユーザーは、Lean が証明の証明書として機能するには定理の記述そのものが正しく表現されていなければならず、これほど広い分野にわたってそれを保証するのは難しいと警告した（直接の引用ではなく、コメントの要旨の要約）（@mathisfun123）。撤回のスレッドでは、その警告が現実になったかのような反応が続いた。「Lean で検証済みではなかったのか」という質問、約400件の結果のうち3件のミスならかなり良い的中率だという反論（@hmate9）、検証の負担はレビュアーに押し付けられ、功績は提案者が持っていくという指摘（@BenoitP）が並んだ（いずれも直接の引用ではなく、コメントの要旨の要約）。

深層分析 — 「証明の希少性」という隠れた前提

Tao のスライドが興味深いのは、この騒ぎを「AI の証明は信頼できるか」という問いとして扱っていない点にある。むしろ彼は逆側から出発する。証明は、他の分野では珍しい性質、すなわち「客観的に検証可能である」という性質を持つ。どの数学が面白いかについては数学者の間で意見が割れても、何が正しく完全な証明かについては広い合意があり、Lean のような証明支援系で書けば計算機が機械的に検査することもできる。さらに証明は高度にデジタル化可能である。物理的な実験も現実世界のデータも要らず、関連文献の相当部分がすでにデジタルで存在している。

Tao の論理はここで反転する。客観的検証可能性、デジタル化可能性、大規模で高品質なデータという三つの性質が重なったおかげで、数学の問題解決は機械学習に特によく適した課題となり、フロンティア AI ラボはこの三つのうち一つでも欠けた他の応用よりも数学を優先した。その結果、我々は「証明の豊富さ（proof abundance）」の時代に入りつつある、というのである。数学の美徳が、そのまま数学の脆弱性になったわけだ。

ここでの核心概念が「証明の希少性（proof scarcity）」である。Tao は、伝統的な数学、すなわち「Math 1.0」の制度、伝統、インセンティブ、公式の目標の多くが、「未解決問題の解を見つけて証明するのは難しく稀であり、相当な人間の専門性を要する」という仮定の上に組織されてきたと見る。そして問題解決は歴史的に研究数学で最も目立つ目標だったが、実際にはより価値のある長期目標の「代理指標（proxy）」だったと言う。希少性の時代には、この代理指標はおおむね正確だった。しかし豊富さの時代にはずれてしまい、問題解決だけを盲目的に最適化することは今や数学の長期的な健全性にとって「積極的に有害」だ、というのが彼の結論である。

この診断の具体的なメカニズムは、スライドよりも Mastodon のスレッドのほうが詳しい。Math 1.0 では、長年の予想に対する画期的な証明は大量の後続活動を生む。著者は講演に招かれ、ワークショップが開かれ、新しい共同研究が生まれ、後続の問題が共有され、若手の数学者がその分野に引き寄せられる。その過程で証明は消化され、洗練され、文脈の中に位置づけられ、最終的には次世代の教科書になる。ところが現在はその逆がしばしば起きている、と Tao は書く。標的が「解決」されればその分野に関心を持たず、結果について質問に答えたり講演したりできるほど AI の出力を理解していない「AI プロンプター」たちが、問題を自律的に解いてしまう。セミナーも共同研究も生まれにくく、その分野に加わる人も少なく、有望な未解決の方向は「先を越される」ことを恐れて公開されなくなっている。

そしてこの過程は不可逆である。一度「解かれた」問題を「未解決」に戻すことはできず、解が存在するという事実だけで、別の経路を探す努力が「汚染」される。Tao はそのため、未解決問題の解が持続不可能なやり方で大規模に「収穫」されており、分野全体の肥沃さが失われていると表現する。スライドの「灯台」の比喩がこの点を支えている。純粋数学の未解決問題は、それ自体が到達すべき目的地ではなく、周辺の地形を探検させる道しるべであり、成功しても失敗しても部分的な進展にとどまっても、その過程で得られる教訓が最終的な解よりも価値を持つことが多い。自動化ツールで灯台に早すぎる到達をすれば、選ばれなかった道の探検が断たれ、周辺分野が「不毛化」しうる、というわけだ。

この論理はソフトウェアエンジニアにも馴染みがある。ベンチマークが学習目標になった瞬間に測定手段としての意味を失うという、グッドハートの法則と同じ構造である。Tao のスライドの Hacker News スレッドでは、あるユーザーが、ソフトウェア開発は成果物が目的なので手段が変わっても産業は崩れないが、数学研究ではプロセスそのものが成果物だという対比を紹介していた（直接の引用ではなく、コメントの要旨の要約）（@theturtletalks）。

展望と示唆 — 何を評価するのか

では Tao は、代わりに何を評価しようと言うのか。Mastodon スレッドの最後の投稿で彼は、Math 1.0 は「当初は十分に理解されていなくても、未解決問題を最初に解いた者」にプレミアムを与えてきたと書き、Math 2.0 は問題解決の役割を脱中心化し、解説（exposition）、共同体の構築、新しい研究方向の開拓をより高く評価すべきだと述べる。さらに数学共同体は、教育、出版、キャリア昇進の基準を明示的に再評価しなければならないと付け加える。「最初に解いた者」の栄誉という古いクレジット体系を正面から狙った言葉である。

スライドはこれを具体例で埋めていく。既知の証明が不透明な結果に動機の明確な説明を見つける「未解決の解説問題（open exposition problems）」、多数の論文を一つの生きたネットワークに束ねる試み（明示的解析的整数論ネットワーク IEANTN）、Mathlib のような大規模で高品質な形式数学ライブラリ、すでに証明された定理から主要な入力を取り除いてもなお証明できるかを調べる「アブレーション研究」、仮定を変えたり外したりしたときに何が救えるかを探る「定理の近傍」の探索などだ。大規模データセットに基づく実験数学も示される。2,200万を超える真偽命題に決着をつけた Equational Theories Project、次数24で可能な25,000のガロア群それぞれに対応する多項式を探す逆ガロア問題チャレンジがその例である。「ケーススタディ」ではなく「母集団調査」という表現が印象的だ。

ここで Lean の位置づけが変わる点に注目したい。Math 1.0 の論理では、形式検証は「この証明は正しいか」を判定する道具だった。Tao の Math 2.0 のリストでは、形式化は Mathlib のように共同体が共有し積み上げる「ライブラリ」として登場する。そして彼の思考実験は、Lean の証明書があっても十分ではないケースを狙っている。AI ががん治療用の化合物カクテルを見つけ、Lean の証明書まで添え、第3相臨床試験を通過したが、誰もその発見の経緯を知らないとしたら、その解は試験手続きや数理モデルの弱点を突いた「ミスアラインした（misaligned）」解である可能性はないのか。Tao はこれを「強力な AI + 人間の理解の欠如 = ミスアラインメントのリスク」と要約する。これは撤回の件と正確に噛み合う。形式検証は記述が正しく移されているという前提の上でのみ意味を持ち、その前提を確かめるのは結局、理解している人間である。

ただし、この思考実験は Hacker News で最も反発を受けた部分でもあった。末期患者なら誰も理解していない治療でも受けるという反応（@qup）、全身麻酔のように作用機序が完全には解明されていない薬がすでに広く使われているという指摘（@squidmaster）が上位に並んだ（いずれも直接の引用ではなく、コメントの要旨の要約）。この反論には一理あるが、Tao の要点を少し外している。彼の四象限は「人間の理解が弱い状態」それ自体を危険とは呼んでいない。それは単にまだ十分に数学化されていない状態にすぎず、危険はその欠如が AI の最適化能力と結びついたときに生じる、というのである。

より鋭い反論は「説明も結局 AI のほうが上手くなるのではないか」というものだ。Tao の Mastodon 投稿を扱った Hacker News スレッドで、あるユーザーは、モデルの知能が上がり続ければ数学者はモデルに証明を段階的に説明させればよく、理解の溝は消えると主張した（直接の引用ではなく、コメントの要旨の要約）（@vasco）。Tao のスライドもこの可能性を排除してはいない。彼が示すリスト自体が、AI を解説やネットワーク構築に使おうというものだからだ。ただし解説が AI で解決されたとしても、「誰が理解したのか」「誰が責任を負うのか」という AGMAI の問いは残る。別のユーザーは、AI は安くないので豊かな国の良い大学が有利になると指摘した（直接の引用ではなく、コメントの要旨の要約）（@contubernio）。評価基準を変えることは、資源配分を変えることと切り離せない。

結論

Tao の「Math 2.0」は、AI の証明が正しいか間違っているかを争う文書ではない。むしろ AI の証明はおおむね正しくありうるという前提から出発し、ならば数学という分野はこれまで何に報いてきたのかを問い直している。彼の答えは「問題解決は代理指標だった」というものだ。希少性の時代には、解決が理解と共同体と後続研究を一緒に連れてきたので、両者を区別する必要がなかった。豊富さの時代には、解決だけが切り離されて出てくる。

同じ週の撤回の件は、その切り離しがどんなコストを生むかを示している。719本の原稿のうち形式化されているのは約42%にとどまり、残りを確かめる責任は事実上、共同体に回される。その共同体が縮みつつある、というのが Tao の警告である。彼が最後のスライドに書いた言葉は意外にも楽観的だ。Math 2.0 の主要なボトルネックは技術でも制度文化でもなく、「想像力」だという。

あなたの分野で「最初にやり遂げた者」に与えてきたクレジットは、何の代理指標だったのか。その代理指標が機械に渡ったとき、本来守ろうとしていたものを何で数えるのか。

出典: