先日、フィールズ賞受賞者であり、カリフォルニア大学ロサンゼルス校（UCLA）数学科教授のテレンス・タオ（Terence Tao）氏がYouTubeで約26分間の実演動画を公開し、Anthropic社が提供するClaude Codeエージェントツールを活用して、Lean定理証明器において数学的証明を形式化する全过程を詳細に実演しました。
（出典：Youtube）
タオ氏は動画の冒頭でタスクの目標を明確にしました：集合論における「シングルトン法則」（Singleton Law）を、非形式化された自然言語の記述から、Leanシステムがコンパイルし厳密に検証できるコードへと変換することです。簡単に言えば、この法則は任意の集合Aと要素xについて、単一要素集合{x}がAに属する条件が、特定の部分集合の性質と等価であることを論証するものです。
数学的概念としては比較的基础的な補題ですが、型理論に基づく厳格なLeanシステムで形式化を行うには、構文要件が極めて高い大量の煩雑なコーディング作業が伴います。
これはタオ氏がこのタスクに初めて取り組んだわけではありません。約9ヶ月前、彼が主導する「方程式理論」（Equation Theories）プロジェクトにおいて、当時の主流ツール（GitHub Copilotなど）を用いて手動でこの証明を完了していました。
（出典：Youtube）
今回Claude Codeを導入してこの問題に再挑戦したのは、タオ氏が新しい世代の「エージェント型コーディングツール」と従来のコード補完ツールとの世代間の違いを直感的に比較したいと考えたからです。
GitHub Copilotが初期にはカーソル位置に基づいて数行のコード自動補完しかできなかったのに対し、Claude Codeはターミナル上で動作するエージェントシステムであり、複雑な自然言語の指示を理解し、自律的にファイルディレクトリを読み込み、手順を計画し、コードの編集と修正を自動的に実行できます。タオ氏の目には、この能力の飛躍的向上は、数学研究における「煩雑な手続き」と呼ばれる反復作業をAIが真に引き継ぐ可能性を示唆しています。
数学界の第一人者もAIを使えば失敗することがある
興味深いことに、動画で示されたスムーズなプロセスは一度で完成したわけではありません。タオ氏は録画の中で、これがClaude Codeを使ってこのタスクを完了させる3回目の試みであると認めています。それ以前には、異なる理由で2回「失敗」していました。
最初の試みでは、タオ氏は「証明全体を完了して」というマクロな指示をClaudeに直接出しました。その結果、AIは45分間連続して稼働し、膨大な量のトークンを消費してコンピュータをクラッシュさせ、最終的に有効な結果を何も生成できませんでした。
あるネットユーザーはコメント欄でAnthropic社に直接@で言及しました：「テレンス・タオに無制限のトークン権限を与えてください。そうすれば数学2.0時代が早く来るかもしれません！」これは冗談のように聞こえますが、現在のAIツールの現実的な問題を突いています：精緻な作業を実際に行うと、トークンの消費速度は本当に速いのです。
（出典：Youtube）
2回目の試みでは、戦略を変更し、AIに補題（Lemma 1, 2, 3）ごとに段階的に実行するよう指示しました。今回は25分で完了しましたが、画面録画ソフトウェアの不具合で保存できませんでした。
最初の失敗の教訓を踏まえ、3回目（今回公開された動画）の実演では、タオ氏は高度に構造化された「スキャフォールディング」（Scaffolding）戦略を採用しました。ファイルの先頭に極めて詳細な「レシピ」（Recipe）を記述し、タスクを初期定義、アウトライン構築、そして3つの補題の段階的証明に分解することで、AIの行動の発散を制約しました。
1. スケルトン構築（Skeletonization）
プロセスの初期段階で、タオ氏はClaude Codeに直ちに導証を進めるのではなく、Leanシステムのプレースホルダーである「sorry」を用いて証明全体のマクロな枠組みを構築するよう指示しました。このステップは異常に順調に進み、AIは非形式化証明における論理的な区切りを正確に識別し、それをLeanコード構造に変換しました。タオ氏は、AIにまず「sorry」付きのスケルトンを書かせ、その後一つずつ埋めていくのが、現時点で最も効率的な人機協調モデルであると指摘しました。
2. 泥沼にはまってと人間による介入
しかし、具体的にLemma 1の証明の詳細を埋める段階になると、Claude Codeの短所が現れ始めました。Leanの基礎論理は極めて厳格であるため、AIは非形式化言語における等式代入に対して「過度に思考する」傾向を示しました。基礎的な数学的定義を頻繁に展開しようとし、人間が与えた手順に従って機械的に推論を進めるのではなくなりました。
動画では、AIはバックグラウンドで大量のバックトラックと自己試行錯誤を行い、計算リソースを大量に消費し、推論過程が異常に長くなりました。この過程で、タオ氏のワークステーションは予期せず一度クラッシュしました。システムが復旧した後、AIが単純なステップを複雑化する窘境に直面し、タオ氏は果断に人間による介入を選択しました。彼は直接キーボードを引き取り、congr（合同/等式置換）命令に基づく戦略を迅速に入力し、僵局を瞬時に突破しました。
彼は客観的に評価しました：「ツールへの過度の依存は、証明に対する直感を失わせる可能性がある。AIが袋小路に入り込んだとき、人間が直接手を動かす方が、AIがエラーを修正するのを待つよりもずっと速いことが多い。」
3. 「並列ワークフロー」の進化
プロセスがLemma 2とLemma 3に進むと、タオ氏は目の覚めるようなワークフローの革新を示しました。AIがスケルトン構築のスキルを習得したことを確認した後、彼は単に「監督者」の役割を演じるのをやめ、AIとの「ダブルトラック操作」を開始しました。Claude Codeがバックグラウンドで自律的に分析しLemma 3の基礎論理を埋めようとする間、タオ氏はコードの前段部分でLemma 2の比較的直感的な「sorry」部分を手動で補完しました。
このような人機並列作業のモデルにより、最終的に総所要時間は約30分以内に圧縮され、最終的なコードはエラーなくLeanコンパイラの厳格な審査を通過しました。タオ氏は、タスクを分割し、人間が一目でわかる論理を処理し、コードを積み上げる必要がある重労働をエージェントに任せるのが、現段階で最も実現可能な実践方法であると総括しました。
AIは「平凡な助教」から「初級協力者」へ
今回の動画をタオ氏による近年のAI実験の歴史の中に位置づけてみると、技術的な飛躍の軌跡が明確に見えてきます。
今回の生成AIブームの初期から、タオ氏は様々なチャットボットを積極的にテストし、それらを「平凡だが完全に無能ではない大学院生」に例えていました。当時のAIは、微積分におけるイプシロン・デルタ極限の証明などを処理する際、幻覚を起こしやすく、変数の領域を頻繁に混同したり、境界条件を見落としたりして、むしろ新奇なおもちゃとして存在していました。
2025年になると、大規模言語モデルの基礎能力の向上に伴い、タオ氏は複雑な学術文献検索におけるGPT-5レベルモデルのパフォーマンスを公開テストしました。そのテストでは、AIは膨大な未構造化論文データベースから特定の定理の起源を迅速に発掘し、彼に数週間の文献調査時間を節約しました。しかし、当時のAIが演じていたのは依然として「上級図書館員」の補助的役割であり、証明の生成に直接関与するものではありませんでした。
そして2026年初頭に入ると、状況が質的に変化しました。ChatGPTに代表される大規模言語モデルは、著名なエルデシュ（Erdős）の未解決予想データベースに本格的に取り組み、数論と組み合わせ論における数百の未解決問題を「独立して」解決しようとしました。タオ氏のGitHubページにも、これらのシステムを用いて周辺的な予想を自動処理する試みが記録されており、人間が精力の限界で見落としていた境界領域を埋めています。
（出典：X）
今回のClaude Codeを用いた実演は、まさに上記の「最先端の探求」と「日常的な実践」をつなぐ架け橋となります。GoogleのAlphaProofが国際数学オリンピック（IMO）の難問を解くほどの公衆向けの演劇性はないかもしれませんが、Leanという型理論が保証する確実性のある環境において、タオ氏の実演はより現実的であり、現代の数学者にとっての真の研究のあり方により近いものです。
もちろん、AIがもたらす効率革命を肯定する一方で、タオ氏と彼が代表する数学界は、技術が現時点で抱える限界を回避していません。
一方で、学界からはAIが生成した証明に高度に依存することで「ブラックボックス化」の問題が持ち込まれるという懸念の声があります。Leanコンパイラが論理の基礎レベルでコードの100%の正しさを保証できたとしても、長大で機械が生成した機械言語は、人間の数学特有の直感的な美しさと可読性を欠いており、数学が「理解の技術」から単なる「記号検証」へと異化される可能性があります。
これについて、タオ氏は科学者特有の客観性と中立性を保っています。彼はAIを強力な「実験数学」ツールとして定義することを傾向しています。計算やパターンマッチングに高度に依存するタスクにおいて、AIは代替不可能ですが、リーマン予想のような破壊的な直感と深い概念の再構築を必要とする核心領域については、人間の主導的地位は依然として揺るぎないものです。
彼が以前IPAM会議で述べた通り：「AIがあなたのために節約した時間が、あなたがそれを修正するために浪費する時間より多ければ、それは成功したツールである。」今回の26分間のノーカット動画は、まさにこの主張の最良の裏付けとなっています。
将来の数学研究において、「人機協作」は新常態となるでしょう。その時には、AIが「初級協力者」として、直観的な構想からコンピュータによる形式化検証に至る数学の瓶首を完全に打通するかもしれません。
参考リンク：
動画URL：https://www.youtube.com/watch?v=JHEO7cplfk8&t=124s
運営/レイアウト：何晨龍