Yakan AI Books

機械は数学を「理解」できるか？ ―テリー・タオと定理証明AIが問いかける知の本質

liberal-arts

  • #数学
  • #人工知能
  • #認識論
  • #証明
  • #テリー・タオ
  • #哲学
  • #形式検証

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

テーマ: 機械は数学を「理解」できるか？

2026年6月8日、Quanta Magazineは「テリー・タオがどのようにAI数学の伝道師になったか」と題する記事を公開した。史上最も偉大な数学者の一人と称されるタオが、AIによるコンピュータ支援証明の熱烈な支持者になったという事実は、数学コミュニティを超えた問いを投げかける。

機械が定理を証明できる時代に、「理解する」とはどういうことか？

本文

テリー・タオとは誰か

テレンス・タオ（1975年生まれ）はオーストラリア出身の数学者で、31歳でフィールズ賞（数学のノーベル賞）を受賞した。解析学・組合せ論・数論・偏微分方程式と、異常に広い分野で最先端の成果を挙げ続けている。数学界で「最後の普遍数学者（the last universalist）」と呼ばれる人物が、今やAIツールを「共同研究者」と呼ぶに至った。

AIによる数学革命が始まった

Quanta Magazineは2026年4月の記事「The AI Revolution in Math Has Arrived（数学のAI革命が到来した）」で、この転換点を詳述した。現在進行中の革命は2種類のAI数学ツールによって牽引されている。

形式証明検証システム （Lean¹、Coq²などの言語）：数学的主張を機械が検証可能な論理式に翻訳し、一行一行を厳密に確認する。人間の数学者が何千ページもの論文を完全に理解できないほど複雑な証明も、機械は漏れなく検査できる。

LLMベースの定理探索システム （大規模言語モデル³を応用）：大量の数学論文を学習し、新しい命題に対して「次に試すべき補題はこれだ」と提案する。数学的直観を模倣する試みである。

タオは特に前者を活用し、自分の研究ノートをLean形式に変換することで「証明の穴」を機械に発見させている。

¹ Lean: Microsoftが開発した定理証明支援システム。数学の命題をプログラムコードとして記述し、コンパイルによって正しさを検証する。
² Coq: フランスのINRIAが開発した同種のシステム。「Coq（コック）」はフランス語で「雄鶏」の意。
³ LLM（大規模言語モデル）: GPTやClaudeのような、膨大なテキストで訓練された言語AI。

証明を「知る」と「理解する」の分裂

ここで哲学的問題が生じる。

数学者ウィリアム・サーストン（William Thurston, 1946–2012）は1994年の論文「数学における証明と進歩について（On Proof and Progress in Mathematics）」で、こう書いた。

「数学における問いは、ある命題が真であることを示すことではない。人々がその命題を理解するようにすることだ。」

この観点に立てば、AIが1000ページの証明を正しいと検証したとしても、それは「証明した」とは言えないかもしれない。誰も理解していない真実は、数学的知識と言えるのか？

AIが「中国語の部屋⁴」のように、意味を理解せず記号を操作しているだけだとすれば、その「証明」はむしろ長い計算である。

⁴ 中国語の部屋（Chinese Room）: 哲学者ジョン・サールが1980年に提唱した思考実験。中国語を全く知らない人が、ルールブックに従って中国語の記号を操作することで、外から見れば中国語を「理解している」ように見える——という状況を指す。機械の「意味理解」への批判として用いられる。

数学の美しさとは何だったのか

一方で、Quantaの別の記事は問いかける。「最も抽象的な数学は世界をより良くできるか？」（2026年3月）。

数学者たちが「美しい」と感じる証明とは、単なる正しさではなく、**なぜそうなるかが一瞬で見える「透明性」**を持った証明である。アンドリュー・ワイルズがフェルマーの最終定理を証明した時（1995年）、その証明は350年来の謎を解いたが、同時に「楕円曲線とモジュラー形式という全く異なる世界がつながっている」という驚くべき洞察を与えた。その「洞察」こそが数学者にとっての価値であった。

AIが証明する定理には、この「なぜそうなのか」という洞察が含まれているのか——それはまだ誰も答えを持っていない問いである。

未来への問い

タオのような天才数学者がAIと協働し始めたことは、実用的な意味では明らかに加速をもたらす。しかし認識論⁵的には、一つの根本的な問いを残す。

人間が理解できない規模の証明が「正しい」と検証されたとき、数学は自然科学と同じ性格を帯びるのではないか。

つまり、「観測（検証）された事実」として受け入れるが、完全には「理解」できない——それはちょうど、私たちが量子力学の実験結果を信じるが、その意味を哲学的に消化できないでいるのと同じ構造である。

AIの時代に数学が向かう先は、「すべてを理解しながら進む」学問から「機械と協働して未知を切り拓く」学問への変容かもしれない。

⁵ 認識論（Epistemology）: 「知識とは何か」「何かを知るとはどういうことか」を問う哲学の分野。

さらに学ぶために

1. ウィリアム・サーストン「数学における証明と進歩について」(1994)

数学の本質を「証明の正しさ」ではなく「人間の理解の共有」に置くサーストンの古典的論考。数学者が「なぜ証明するのか」を問い直す。

2. サイモン・シン「フェルマーの最終定理」(1997, 邦訳:新潮文庫)

350年間未解決だった命題に挑んだアンドリュー・ワイルズの7年間の孤独な証明の旅。「数学的証明とは何か」を一般読者に伝える最良のノンフィクション。

3. Quanta Magazine「The AI Revolution in Math Has Arrived」(2026)

AIが数学の世界に何をもたらしつつあるかを、Lean形式証明システムとLLM定理探索の実例とともに解説した最新レポート。

参考