【geek-terminalニュース】Terence TaoのMath 2.0とAI数学計算資源論の最新情報

【事象の全貌と背景】
以前お伝えしたOpenAI数学原稿722本公開と、AI生成証明の大量流入をめぐるMathocalypse論争の続報です。ただし今回は、OpenAIの原稿そのものではなく、Terence Tao氏がCaltechで行ったとされる「Math 2.0」講演スライドと、そこから派生した「AI数学にどこへ計算資源を投じるべきか」という議論が中心です。

公式・大手メディア側で確認できる中核は、Tao氏がAIによる数学問題解決の進展そのものを単純に拒否しているのではなく、AIが出した結果を人間の数学共同体が理解し、説明し、質疑し、研究文脈へ接続できるかを問題にしている点です。TechCrunchは、AI出力が数学界の標準をまだ満たしていないという文脈でTao氏の批判を紹介し、OpenAI Developer Community側の整理でも、Math 2.0は個別問題の解決能力だけでなく、説明、共同体形成、新しい研究方向の開拓を重視する枠組みとして扱われています。

ここでギーク的に熱いのは、「AIが証明を書けるか」から「数学という探索空間を、計算資源でどう測量するか」へ論点がズレたことです。証明は希少資源だった。だからMath 1.0の制度、査読、名誉、問題設定、教育は、だいたい「難問を解いた人が偉い」という重力で回っていた。ところが、強力なモデルと大量computeが入ると、証明は豊富になる可能性がある。するとボトルネックは、証明の発見ではなく、何を探索すべきか、失敗結果をどう記録するか、どの証明が人間の理解を増やすか、どの形式化が次の発見を生むかに移る。

【技術的ディープダイブ】
Tao氏のスライドで重要なのは、数学がAIに向いている理由をかなりエンジニアリング寄りに分解している点です。数学の証明は、主観的な評価が絡む多くのタスクと違い、正しさを客観的に検証しやすい。さらにLeanのような証明支援系に落とせば、機械的チェックが可能になる。物理実験や現実世界データを必ずしも必要とせず、既存文献や定義ライブラリをデジタルに参照できる。この「検証可能、デジタル化可能、高品質データがある」という3点セットが、AIラボに数学を優先ターゲット化させている、という見立てです。

数値面でも、単なる思想スライドではありません。Equational Theories Projectでは、普遍代数における2200万超の真偽命題を、人間と自動化された議論のクラウドソースで処理した例が挙げられています。Inverse Galois Problem challengeでは、degree 24の多項式について、25,000通りの可能なGalois群を探す第1段階が成功し、次はdegree 31への拡張が共同作業として示されています。さらに2026年11月13日から15日に予定されているCaltech Mathathonは、既存証明が不満足な結果に対して、オープンソースAIツールで新しい、または改善された証明を探す実験として紹介されています。

ここでの計算資源論は、GPUを積んで未解決問題を殴るだけの話ではありません。むしろ、失敗した試行も含めた透明なベンチマーク、Lean証明、Mathlibのような形式数学ライブラリ、論文群を生きたネットワークとして統合する仕組み、既存定理から仮定を抜いてどこまで保てるかを見るアブレーション研究、定理近傍を自動探索するワークフローにcomputeを回す、という話です。AI数学は「答え自販機」ではなく、探索ログ、検証器、研究地図、説明生成器、共同体インフラを束ねる計算科学になりつつある。

【コミュニティの生々しい熱量と議論】
Redditでは、この話がかなり荒れています。r/singularityでは「TaoはAI数学にもっと計算時間を使えと言っているのに、反AIとして誤読されている」という投稿が伸び、Tao氏の立場をAI拒否ではなく、計算資源の使い道の再設計として読む流れが出ています。ただしこれはコミュニティ側の読み替えであり、公式確認済みの事実としては扱えません。

反応の温度差がすごい。あるユーザーは「imagination is the bottleneckという結論を真面目に受け取るのが難しい」と疑問を呈し、別のユーザーは「彼の例、たとえばアブレーション研究は趣味の数学好きにもかなり面白い」と評価しています。HNでは「Mathematicians don’t own math」という所有権への反発と、「compute isn’t gonna turn AI slop into a clear, readable paper」という冷笑が並びます。lobste.rsでは「Feels identical to what is happening in software to me」と、ソフトウェア開発で起きているAIコード大量生成とレビュー負荷の問題に重ねる声も出ています。

最も燃えたのは、AIが癌治療のような高リスク領域で「動く答え」を出したとして、人間が理解していなくてよいのか、という思考実験です。コミュニティでは「誰が理解しているかなんて患者は気にしない」という反発と、「Taoは治療を拒否しろと言っているのではなく、なぜ効くか、長期副作用は何かを理解する努力を捨てるなと言っている」という擁護がぶつかりました。ここは数学に限らず、AIが形式的な合格証明やテスト通過結果を出したとき、それを現実の信頼へどう変換するかという、エージェント時代の根本問題でもあります。

【今後の展望とエコシステムへの影響】
今後オワコン化しそうなのは、「AIが難問を解いた」という単発プレスリリースだけで価値が決まる世界です。TechCrunchやOpenAI Developer Communityで確認できる整理に従えば、争点はAIが数学を解けるかどうかではなく、その成果を人間が検証し、説明し、教育し、次の研究へ接続できるかです。つまり、単なる証明生成ランキングより、証明の可読化、形式検証、失敗例の共有、探索空間の地図化、研究共同体への吸収能力が価値を持つ。

エコシステム的には、LeanとMathlibはますます重要になります。ただしLean証明があるだけで勝ち、という単純な話でもない。形式検証は「正しい」を支えるが、「なぜ重要か」「何を一般化できるか」「どの分野に橋を架けるか」は別問題だからです。ここに、AIによる文献ネットワーク化、定理近傍探索、アブレーション、説明生成、オープンな数学モデル開発が重なると、数学研究はCI/CD的なパイプラインと、研究者の審美眼が混ざった新しい形になります。

今回のMath 2.0論は、AI数学を「人間数学者 vs AI」という雑な対立から救い出している点が重要です。計算資源を投入すべきなのは、難問の首級を取る競争だけではない。人間が見落としていた地形を測ること、既存証明の不透明さを剥がすこと、失敗した探索を資産にすること、共同体が読める知識へ変換すること。AI数学の本番は、証明を吐かせるプロンプト芸ではなく、数学そのものを探索可能なインフラに作り替えるところにある、というわけです。