AI時代の数学──ICM 2026でテレンス・タオが示した見取り図

2026年7月24日、カリフォルニア大学ロサンゼルス校教授でフィールズ賞受賞者のテレンス・タオが、フィラデルフィア（ペンシルベニア・コンベンションセンター）で開かれたICM 2026において講演「Mathematics in the age of AI」を行った。公式サイトで公開されたスライドは、「数学基礎論の危機」（1900〜1930年）という歴史的背景を振り返ったうえで、新しい危機を提起する。今度は公理をめぐる危機ではなく、数学者コミュニティの価値観と実践をめぐる危機である。タオが立てる「Community Response Question」は伝統的な数学の問いではなく、メタ数学的・政治的・倫理的・文化的な問いであり、彼はそこで「AI Capability Conjecture」（道具がどれほど有能か）を、この分野が何を目指し何を大切にするのかという問いから切り離している。

タオは、この予想のさまざまな形について賛否を論じる際に持ち出される多くのデータが、統制された科学的条件のもとで集められたものではないこと、そして公開されている証拠が選択バイアス、非科学的なインセンティブ、開示されないコストを抱えていることを指摘する。唯一の例外として挙げられるのが独立プロジェクトFirst Proof（1stproof.org）だ。その第2ロットの10問は2026年5月28日に統制された条件下で4つのAI「ハーネス」に対して試験され、10問中7問が少なくとも1チームによって出版水準の品質で解かれた。正しさと記述については専門家の査読が行われている。結果はarXivのプレプリント2606.18119とハーバード大学Center of Mathematical Sciences and Applicationsのページに記録されている。とはいえ10問というサンプルにとどまり、数学研究全体に一般化できるものではない。試験された4つのハーネスがどの商用システムに対応するかも確認されていない。

講演の要になっているのは、数学的生産を5つの段階──生成、検証、記述、出版、正典化──に分解する視点だ。タオによれば、AIと自動形式化の支援系（Rocq、HOL、Lean）はすでに最初の2段階を加速させたが、後の3段階は依然として人間の仕事が支配している。タオはerdosproblems.com上のAIによる証明にも触れる。そこでは解答が人間の査読者によって検証されておらず、信頼性の問題が具体的な症状として現れている。さらに彼は自動的な記述を批判する。「自然な摩擦」──人間の著者がぶつかる困難──が読者に有用な手がかりを与えるのに対し、AIによって滑らかに磨き上げられすぎた証明はその手がかりを奪いかねない、というのだ。タオはこう述べている。「In short, we will transition from an era of proof scarcity to an era of proof abundance」。

タオはLeiden Declaration on Artificial Intelligence and Mathematics（2026年6月2日）を引き、実践的な指針を示す。もし著者たちが自分の結果について、明快で専門家水準の講演を説得力をもって行えないのなら──内容が正しく、帰属も適切であるという条件を満たしたうえで──その結果は出版されるべきではない、というものだ。結論として彼は、問題解決についての分析は教育、メンタリング、採用、研究資金にまで広げられるべきであり、教育課程でのAI利用は厳しく制限すべきだと述べる。最後に一点。この講演の公開文書はスライドであり、話された内容の公式な書き起こしは存在しない。