2026年10月、カリフォルニア工科大学の演台に立った数学者テレンス・タオは、直感に反する重大な警告を発した。現代のAIは数学研究をかつてない逆説へと導いている。およそ一世紀にわたり続いてきた「証明の希少性」は、いまや「証明の過剰」へと急速に反転しつつある。
過去100年間、数学の基盤は「証明を得ることは極めて困難である」という前提に立脚していた。AIはその大前提を根底から覆そうとしている。問題を解くことは本来、学問の前進を測るための指標にすぎなかった。しかし今や、問題解答そのものを究極の目的に据え続けることが、この学問そのものを空洞化させかねない。
年間2200万件の命題を判定、問題解答はもはや希少ではない
伝統的な数学は「証明の希少性」の上に築かれてきた。未解決予想を一つ攻略するために、一流の専門家が何年もの歳月を捧げることも珍しくなかった。大学の教員審査、学術誌の出版、研究者の名声といった学界全体の仕組みも、この希少性を軸に機能してきた。
しかし、その需給バランスは膨大な計算資源によって塗り替えられつつある。タオは講演の中で具体的な実績を提示した。Equational Theories Projectは2024年から2025年にかけて、人間と機械の協働を通じて普遍代数学における2200万件以上の命題の真偽を判定した。
図：Equational Theories Projectはクラウドソーシング手法によって2200万件以上の命題を判定した。出典：テレンス・タオ「Math 2.0」講演スライド
同様の加速は他の分野でも起きている。2026年の逆ガロア問題チャレンジでは、共同研究チームが短期間のうちに次数24の全25,000個のガロア群に対して多項式を算出し、その後プロジェクトは次数31へと対象を拡大した。
この圧倒的な処理能力は、手作業による推論の工期を根本から覆した。莫大な計算資源が投じられた結果、数学研究は孤立した定理を解剖する職人芸から、データ駆動型の全数調査（国勢調査）へと変貌を遂げつつある。
客観的に検証可能で実験不要、数学は大規模モデルの理想的訓練場と化した
なぜフロンティアAI研究所は、生物学や社会科学よりも純粋数学を熱心に選ぶのか。その根本的な理由は、純粋数学が備える極めて稀な二つの工学的特性にある。
第一の特性は、客観的検証可能性である。数学者はどの予想がより重要であるかについては議論するが、導出された結論が正しいかどうかについては盤石な合意を持つ。Leanなどの対話型定理証明支援系を用いれば、コンピュータはコードレベルで機械的に論理展開を検証できる。
第二の特性は、高度なデジタル自己完結性である。数学的証明には物理的な実体も、現実世界からのノイズ混じりの入力データも、出力を検証するための実験施設も不要だ。紙とペン、形式化された数学ライブラリ、そしてデジタル化された膨大な文献があれば、機械学習はこの閉じたループの中で何度でも反復訓練を行える。
この条件を兼ね備えた領域は極めて少ない。そのため先端AI研究所は、多くの実用タスクよりも数学の問題解答能力を優先してきた。競技スコアは機械で自動判定でき、プレスリリースでも見栄えのする数値を提示できるからだ。
しかし、モデルの推論能力には激しいムラが存在する。潤沢な計算資源を与えれば専門家の手を借りずに難問を突破できる一方で、複雑な対話や現実世界の生きた経験を必要とする実務タスクでは、AIは依然として容易に立ち往生する。
ソーシャルメディア上の印象はさらに歪んでいる。目にするのはAIが解いた成功例ばかりだ。タオが指摘するように、現在の数学のフロンティアにある大半の問題は、どれほど計算資源を投じても未解決のままである。数学の問題空間は無限であり、難易度の上限も存在しない。First Proofのような検証基盤が設立されたのはまさにそのためであり、投じた計算資源や失敗した試行結果も含めた全面的な公開を求めている。
到達点をすべてと錯覚すれば、周辺の生態系は踏み荒らされる
純粋数学の世界において、未解決問題は単にこじ開けられるのを待つ鍵穴ではない。タオは示唆に富む比喩を示した。未解決の難問とは、未知の海原にそびえ立つ灯台のようなものだ。
灯台の真価は、周囲の航路を照らし出すことにある。そこへ向かって航海するプロセスこそが、最終的な解答よりもはるかに豊かな実りをもたらす。成功、失敗、あるいは途中で頓挫した試行のすべてが、後世に残る教訓となる。
図：Math 1.0からMath 2.0への研究フロンティアの進化。出典：テレンス・タオ「Math 2.0」講演スライド
自動化ツールを用いていきなり灯台の頂点へ到達してしまうと、その途中の海路を航行する者はいなくなる。本来であれば試行錯誤の過程で育まれるはずだった理論、道具、そして数学的直観は、生まれる契機を失ってしまう。こうして「問題解答」と「真の理解」は完全に切り離される。
治験をパスした抗がん剤の処方箋、誰も機序を知らぬまま血管に投与できるか
歴史的に見ても、問題解答は理解の深さを測るための代理指標にすぎなかった。証明が希少だった時代には、大問題を解決することは常に壮大な理論の誕生を伴っていた。しかし証明が過剰になった現代では、力まかせの探索によって代理指標と本質的な目的が直接乖離してしまった。
タオは講演の中で一つの思考実験を提示した。ある先端研究所がAIモデルを訓練したとしよう。その目的は極めて明快で、第III相臨床試験を一切の誤りなく通過できる抗がん剤の処方箋を出力することだ。
莫大な計算資源を消費した後、モデルは未知の化合物処方と、厳密なコードによる証明を提示した。現実の臨床試験でも、その処方は見事に試験を通過した。しかし、分子レベルでなぜそれが効くのかを理解している科学者は一人もいない。
もし自分自身が初期のがんと診断され、機械がその処方を提示したとき、その液体を静脈に注入する前に、少なくとも誰か一人の人間が——たとえ一部分であっても——作用機序を理解していてほしいと願わないだろうか。
純粋数学の検証思想は、いずれ現実世界へと波及する。ブラックボックスの答えに寄りかかって人間が思索を放棄することに慣れてしまえば、応用科学を支える安全の基盤もまた、音を立てずに崩壊していくだろう。
テレンス・タオの処方箋：計算資源を「問題を解くこと」から「人間の理解を助けること」へ
機械がもたらした過剰の危機を前に、タオが提示した処方箋は「Math 2.0」への転換である。その核心は、ツールの力点を単方向の力まかせな解答から、人間の理解を拡張する方向へと再配置することだ。
その代表例が「オープン解説問題（Open Exposition Problems）」と呼ばれる新たな試みである。形式的な証明は得られているものの、論理の展開が晦渋で直感に乏しい結果に対し、動機づけが明確でわかりやすい説明を見つけ出す作業だ。カリフォルニア工科大学で改編されたMathathonは、この方向性に向けた最初の実験である。
研究ネットワークとコードベースの構築も加速している。明示的解析数論ネットワークは散在する学術論文を有機的な知識グラフへと結びつけ、形式化数学ライブラリMathlibはアルゴリズム検証のための共通基盤を提供する。
また研究者たちは、計算資源を活用して「定理のアブレーション実験」にも着手している。ある定理の決定的な前提条件を取り除いたときに結論が維持できるかを観察したり、条件を緩和して周辺の派生空間を探索したりする試みだ。
こうした取り組みは、計算資源を新たな方法論の抽出に充て、人間が知識の地図全体を鮮明に見渡せるようにすることを目的としている。
タオの目には、Math 2.0を前進させる最大のボトルネックは計算資源でも組織文化でもなく、人間の「想像力」の不足であると映っている。
参考リンク：
- テレンス・タオ カリフォルニア工科大学講演「Math 2.0」講義ノート・スライド
- First Proof 形式数学ベンチマークプラットフォーム (1stproof.org)
- Equational Theories Project クラウドソーシング共同研究アーカイブ
- 逆ガロア問題チャレンジ (IGP24) 共同作業記録
