AIが未解決の数学的難問を解き明かす日は来るのか——。そんな巷に溢れる好奇心丸出しの、あるいは終末論的な議論は、一旦脇に置いておくこととしよう。
DeepMindのAlphaProofが国際数学オリンピック（IMO）レベルの難問を解き、Large Language Model (LLM) とLeanなどの定理証明支援系（Proof Assistant）が結合される現状を見れば、AIが遠からず「研究レベルの数学的タスクを、ある程度の自律性と精度で遂行できるようになる」という仮説（Terence Taoが言うところの “Working Hypothesis”）は、もはや疑うよりも前提として受け入れた方が生産的である。
我々が直面している真の危機は、「AIに数学ができるか」という技術的検証ではない。AIという異次元の最適化マシンを前にして、「そもそも数学という営みの真の目的と価値は何であったか」を、我々自身が言語化できていないというパラダイムの危機である。2026年国際数学者会議（ICM）におけるTerence Taoの講演、および近年のAIと数学を巡る議論（Leiden Declarationなど）を紐解きながら、AI時代における数学コミュニティの構造的変容と、迫り来る「証明の過食症（Proof Indigestion）」について考察する。
真理の基礎から、価値の基礎へのストレステスト
歴史を振り返れば、数学という学問は過去にも似たような激動を経験している。20世紀初頭、数学者たちは集合や無限といった概念を「素朴に」扱っていたが、RussellのパラドックスやGödelの不完全性定理によって、その暗黙の前提は根底から覆された。結果として生じた「基礎の危機（Crisis in foundations）」は数学界に大混乱をもたらしたが、最終的には現代の我々が依存する強固で厳密な公理的枠組みを生み出した。
現在進行形のAIによる変革は、これに匹敵する歴史的転換点である。ただし今回ストレステストに晒されているのは、数学的「真理」の基礎ではない。我々が何を数学的貢献とみなし、何を評価し、誰（あるいは何）がその仕事をしたとみなすのかという、これまで暗黙の了解として済ませてきた数学的「価値」と「実践」の基礎である。
これまで、数学の目的は多岐にわたっていた。未解決問題を解くこと、新しい理論を構築すること、コミュニティを形成すること、次世代を育成すること、そして永続的な美を創造すること。幸福なことに、歴史上これらの目標は常に「正の相関」を持っていた。難問を解こうと苦闘する過程で新理論が生まれ、それに惹かれた学生が育ち、コミュニティが形成される。だからこそ我々は、「未解決問題を解く」という単一のわかりやすい指標を、全体の健全性のプロキシ（代替指標）として無邪気に利用し続けることができた。
しかし、ここにAIが介入すると事態は一変する。生成AIは、真の理解を伴わずに「それらしい出力」を生成することに長けた、地に足のつかない（ungrounded）最適化装置である。Goodhart’s Law（グッドハートの法則：「ある指標が目標にされたとき、それは良い指標ではなくなる」）が教える通り、AIが「問題を解くこと」や「論文を量産すること」に過剰に最適化された瞬間、これまで揃っていた数学の多様な目標は無惨にも乖離し始める。
「自然な摩擦」の喪失と、証明のパイプラインの崩壊
問題解決という単一のタスクを例に取ろう。我々の目標は単に「問題を解く」ことではない。これまでは以下のような暗黙のパイプラインが存在していた。
- 生成 (Generation): 解答を生み出す。
- 検証 (Verification): それが正しいか確認する。
- 説明 (Exposition): 他者が理解できるように書く。
- 受容 (Acceptance): コミュニティがそれを消化し、価値を認める。
- 正典化 (Canonicalization): 洗練され、教科書に載るような普遍的理論に組み込まれる。
AI、特にLeanのような形式的検証システムと結合したAIは、ステップ1と2を爆発的に加速させる。著者の権威や勤勉さに依存しない、数学的に100%正しい（検証済みの）証明が、安価なコンピューティング・リソースによって大量生産される時代の到来である。「証明の希少性（Proof Scarcity）」を前提に設計されてきた我々の学術システムは、この「証明の過剰（Proof Abundance）」に耐えられない。
さらに厄介なのが、ステップ3の「説明」である。現在のAIが生成する数学的テキストは、文法やフォーマットこそ完璧（あるいは完璧すぎる）だが、本質的な議論の新規性と、どうでもいい自明な計算を同じトーンで平坦に記述しがちだ。
Terence Taoはここで、人間の書く証明には「自然な摩擦（Natural Friction）」が含まれていると看破する。人間が苦労した箇所には、言い訳がましい注釈が入ったり、記法が突如として慎重になったり、何度も書き直された痕跡が残る。この「摩擦」こそが、読者に対して「ここはスピードを落として注意深く読め」というシグナルとなり、分野の暗黙知を伝達する重要なチャネルとなっているのだ。AIによって過剰に研磨され、摩擦を奪われたツルツルの証明は、表面的に読みやすくても、人間にとって極めて学習しにくい代物となる。
そしてステップ4の「受容」とステップ5の「正典化」に至っては、純粋に人間的で、遅々として進まないプロセスである。自動化されたフィルターで論文を弾くことはできても、コミュニティ全体でその定理を咀嚼し、共有財産として血肉化する作業はAIには代替できない。息をするように証明を量産するAIを前にして、無償のボランティア労働に依存する現在の査読システム（Peer Review）は物理的に崩壊するだろう。
The Theorem Economyからの脱却
では、どうするべきか。2026年に発表された「Leiden Declaration on Artificial Intelligence and Mathematics」や、Committee on Publication Ethics (COPE) などのガイドラインは、その一つの指針を示している。
大前提として、AIは法的責任を負えない非法人であるため、論文の著者や共同著者にはなり得ない。著作の責任はあくまで人間が負う。その上で、AIツールの使用は透明性をもって開示されなければならない。
しかし、より本質的なルールとしてTaoが提唱するのは、「もし著者が、その結果について明確に、専門家レベルの講演を行い、適切に帰属を示すことができないのであれば、その結果は出版されるべきではない」という経験則である。たとえLean上で形式的に100%検証された証明であっても、人間の専門家がその論理展開を「自分自身の言葉で」説明し、コミュニティに消化させることができないのであれば、それは不完全な仕事とみなすべきなのだ。
これは、数学界の評価軸の根本的な転換を意味する。いち早く証明を生成し、「最初に解いた」という先取権を奪い合う「The Theorem Economy（定理の経済）」の時代は終わる。AIが無限に定理を生成できる時代において価値を持つのは、証明を生成すること自体ではなく、それを人間の知識体系に繋ぎ合わせ、コミュニティが消化可能な形に翻訳し、正典化する（Canonicalization）という、泥臭くも人間的なプロセスの方である。
終わりに：開発者とコミュニティの対話に向けて
AIによる数学研究の自動化は、我々に「人間が数学をやる意味」を鋭く突きつけている。教育の現場においても、AIは個別化された強力な学習サポートを提供する一方で、解答を自動生成させるだけのツールに成り下がる危険性も孕んでいる。「数学者を育成することの目的は、宿題の正しい解答を作成させることではない」という自明の理が、今ほど重みを持つ時代はない。
数学コミュニティは、このパラダイムシフトから目を背けるべきではない。AIの能力を過大評価して絶望するのも、過小評価して既存のシステムにしがみつくのも、等しく知的な怠慢である。AIツールがどのような出力をもたらすのかを冷徹に見極めると同時に、我々自身がこれまで無自覚に信奉してきた「目標と価値」を再定義し、オープンな議論を通じて新たなワークフローとインフラを構築していく。その痛みを伴う自己変革の先にしか、AI時代の数学の未来はない。