教養を深める1本 — 2026年6月11日

テーマ: 証明とは何か?

── テリー・タオがAIに惚れた理由、そして数学的真理の変容

「AIが使えるレベルの自動化と、それが『スラッジ(雑多なゴミ)』に成り下がるまでの境界は、どれだけ検証を厳格にできるかに比例する」 — Terence Tao (2026)

数学者の王が転向した

Fields Medal[^1]は数学界のノーベル賞である。受賞者の多くが40歳前後の「若き天才」であることも特徴だ。その受賞者の中でも「生きている数学者の中で最も優れている」と多くの専門家に評されるのが、オーストラリア系アメリカ人のTerence Tao(テリー・タオ、51歳)だ。

彼が2023年10月に自身のSNSに書いたのは、数学界にとって小さな地震だった。「とうとうLean4[^2]を試してみることにした。AIに助けてもらいながら」。

それから2年半。2026年6月8日のQuanta Magazine記事は彼が「AIの布教者になった」と表現した。

なぜ彼はAIに惚れたのか

数学における「探索コスト」という概念から始めよう。

数学者は証明を書く前に、何時間も「このアイデアは正しいだろうか」という探索をする。方向が間違っていれば、すべてが無駄になる。この探索コストの高さが、数学をきわめて保守的な営みにしてきた理由の一つだ。

タオが発見したのは、AIがこの探索コストを劇的に下げるということだった。「AIのおかげで、もっとクレイジーなことを試せるようになった」と彼は言う。アイデアが30秒で失敗と判明するなら、10個の的外れなアイデアを試しながら1個の正解に辿り着ける。天才が持つ「鋭い直感」の補完として、AIが「安価な実験台」になった。

しかし彼が最も重視したのは探索側ではなく、検証側だ。

信頼の問題: 「正しい」とはどういうことか

数学の歴史には、長年「証明された」と信じられていた定理が実は穴だらけだったと判明した例がある[^3]。人間の目で検査する証明は、どれほど優秀な査読者がいても完璧ではない。

そこで登場するのが形式証明検証ツール「Lean」だ。Leanはプログラミング言語の一種で、数学的証明を一行ずつ機械的に検証する。人間の「なんとなく正しそう」という直感が介在する余地がない。

タオの言葉は示唆に富む。「AIの自動化をどこまで使っても『スラッジ』にならないかは、どれだけ厳格に検証できるかに比例する」。AIに任せれば任せるほど、検証の网が細かくなければならない。AIを信頼するために、もう一つの機械(Leanコンパイラ)が必要になる。

これは哲学的に興味深い構造だ。人間の権威による証明の保証 → 機械による形式検証の保証 という移行が起きている。

協調の革命: 信頼なき共同研究

タオがAIと形式証明に惹かれるもう一つの理由が、「信頼なき協調」だ。

従来の数学的コラボレーションは、互いの専門性と誠実さへの信頼に依存していた。世界規模の分散協力は、信頼関係の構築コストが高すぎて困難だった。

ところがLeanで書かれた証明コードはコンパイラが検証する。「見知らぬ人が書いたコードでも、コンパイラが通れば正しい」。これは、オープンソースソフトウェアのコードレビューに近い文化を数学にもたらす。何百人もの数学者が同じ問題を分割して取り組み、Leanが各ピースを検証し、全体を組み立てる——「通常の数学では不可能な規模の研究」が見えてきた。

数学的真理の「民主化」と「機械化」の矛盾

ここで問いを立てたい。機械が検証した証明は、本当に数学的「真理」なのか?

歴史を振り返ると、「証明の信頼性」は時代によって変わってきた。

• 古代ギリシア: 論理的演繹。ユークリッドの「原論」が2000年の権威を持った
• 19世紀: 無限の概念が曖昧なまま使われていた「証明」が厳密化され、多くが書き直された
• 20世紀: コンピュータ支援証明の登場。四色定理(1976年)は人間が確認できない大量の場合分けをコンピュータが処理した

その都度「これは本当の証明か?」という議論が起きた。そしていつも数学は新しい基準を飲み込んで前進した。

2026年の問いは: 証明の「創造性」はどこに宿るのか。AIが探索を代行し、Leanが検証を代行するなら、数学者に残るのは何か?

タオの答えは明快だ。「問いを立てること」だ。何を証明したいか、どの方向を掘るべきか、どんな問いが美しいか——それは依然として人間の仕事だ。AIは「解く」ことを安くするが、「何を解くか」を問う知性は、まだどの機械も持っていない。

今日から始める探求

この問いは数学を超えて普遍的だ。あらゆる知識労働で「探索」と「検証」が分離され、後者が自動化されていく。残るのは「問いを立てる能力」だ。タオの転向は、天才が最も人間的な部分に撤退した物語でもある。

さらに学ぶための3点

1. Terence Tao本人のブログ「What's New」

タオが自分の数学的思考と、AIに関する考察を直接綴っているブログ。2026年3月29日の「Mathematical methods and human thought in the age of AI」は必読。 https://terrytao.wordpress.com

2. 書籍「数学する精神」(加藤文元著, 中公新書)

数学的証明とは何か、美しい証明と醜い証明の違いは何かを日本語で丁寧に解説した入門書。形式証明と人間の直感の関係を考えるための土台になる。

3. Quanta Magazine "The AI Revolution in Math Has Arrived" (2026/4/13)

AIがどのように数学的証明に使われ始めたかを、具体的な結果とともに報告した記事。2025〜2026年の動向が俯瞰できる。 https://www.quantamagazine.org/the-ai-revolution-in-math-has-arrived-20260413/

[^1]: Fields Medal: フィールズ賞。4年に1度、40歳以下の数学者に贈られる数学界最高の賞。

[^2]: Lean4: Microsoftが開発に関わった形式証明支援システム。数学的証明をプログラムコードとして記述し、コンパイラが正しさを検証する。

[^3]: 例: 19世紀のラクロワ、コーシーらによる解析学の証明の多くは、後に「δ-ε論法」の観点から不完全と判明し書き直された。