最後の数学者たち - - YouTube動画の解説

最後の数学者たち

オートダビング版

Curt Jaimungal

チャンネル登録者数 56.3万人

メンバーになる

チャンネル登録

293,166回視聴 2026/08/11 Theories of Everything with Curt Jaimungal

私は個人的にエコノミスト誌を購読しています。TOEリスナーは年間購読料が35%オフになります。こんな特典は他のポッドキャストにはありません！ https://economist.com/TOE 全エピソードを数日早く、広告なしで、さらに私のエッセイも配信しています。 https://curtjaimungal.substack.com/su... 数学界最高の栄誉であるフィールズ賞受賞から10日後、ジェイコブ・ツィメルマン氏が、OpenAIのAI安全チームに一時的に移籍する理由、そしてその決断をしながらもなお悲しみを抱えている理由について語ります。この対談では、数学がAIによって根本的に変革される最初の分野の一つである理由、誰も理解できない証明は果たして有効なのか、数学における「理解」とは一体何を意味するのか、最先端のモデルへのエリート層のアクセスに関する倫理、ライデン宣言に対する彼の見解、そして急速に進化するAIの時代に純粋数学のキャリアを考えている若者へのアドバイスなどについて語ります。これはジェイコブ・ツィメルマン氏との初の独占ポッドキャストです。 背景にある絵画（残念ながら見えませんが…私のミスです！）は、才能あふれるアーティスト、クリス・デビッドソン氏の作品です。彼女の作品はぜひこちらでチェックしてみてください：  / hellokrisdavidson   フォロー：

• Spotify：https://open.spotify.com/show/4gL14b9...
• Substack：https://curtjaimungal.substack.com/su...
• Twitter：  / toewithcurt  
• Discord招待：  / discord  
• 暗号通貨：https://nowpayments.io/donation/TOE
• PayPal：https://www.paypal.com/donate?hosted_...

タイムスタンプ：

• 00:00:00 - フィールズ賞と悲しみ
• 00:05:38 - 典型的な人間の認知パターン
• 00:10:40 - プロンプト数学の未来
• 00:15:40 - 純粋数学と物理学のループ
• 00:21:00 - 認識論的ブラックボックス
• 00:26:00 - 直観を超える厳密性
• 00:31:20 - 理解の認知メカニズム
• 00:37:00 - ゲーデルとワーキングメモリ
• 00:42:10 - 即興芸術としての数学
• 00:47:30 - AIの力と実力主義
• 00:52:50 - 数学の危機
• 00:58:20 - 無制限最適化のリスク
• 01:03:40 - AI安全マンハッタン計画
• 01:08:50 - AI後のキャリアのためのトレーニング
• 01:14:10 - マネジメントのシフト
• 01:19:40 - 認知負荷軽減と適応

言及されたリンク：

• ジェイコブのウェブサイト：https://www.math.utoronto.ca/~jacobt/
• ジェイコブの論文：https://www.semanticscholar.org/autho...
• Quanta誌のジェイコブに関する記事：https://www.quantamagazine.org/jacob-...
• アンドレ＝オールト予想：https://www.ams.org/journals/notices/...
• 志村多様体とアンドレ＝オールト予想に関する論文： https://arxiv.org/abs/2109.08788
• O-最小GAGAとグリフィス予想 [論文]: https://arxiv.org/pdf/1811.12230
• 数学と理論計算機科学における10の進歩: https://openai.com/index/ten-advances...
• ライデン宣言についての考察: https://gowers.wordpress.com/2026/07/...
• トビアス・オズボーンのLinkedIn投稿:   / tobias-osborne-601830a5_farewell-to-the-co...  
• Math For AIの安全性：https://mathforaisafety.org/
• チャールズ・フェファーマン：https://en.wikipedia.org/wiki/Charles...
• G関数、動機、そしてありそうもない交点 [論文]：https://arxiv.org/abs/2501.09867
• トビアス・オズボーンのQFT講義：   • Quantum field theory  
• AISIウェブサイト：https://www.aisi.gov.uk/
• セバスチャン・ジャイムンガル：https://sebastian.statistics.utoronto...
• エドワード・フレンケル [TOE]：   • Revolutionary Math Proof No One Could Expl...  
• ロジャー・ペンローズ [TOE]：    • Roger Penrose: "My Crazy Idea That Explain...  

その他のリンクはこちら：https://curtjaimungal.substack.com ゲスト出演料は無料です。#科学

制作の裏側

オートダビング

いくつかの言語の音声トラックが自動生成されました。 詳細

---

カート・ジェイムンガル（Curt Jaimungal）氏の人気ポッドキャスト『Theories of Everything (TOE)』における、ジェイコブ・ツィメルマン（Jacob Tsimerman）教授との対談動画『最後の数学者たち』についての解説です。

2026年の国際数学者会議（ICM）で最高峰の栄誉であるフィールズ賞を受賞したわずか10日後に、OpenAIのAIアライメント／AI安全性チームへ一時移籍することを発表したツィメルマン氏。数学界の頂点に立った人物が、なぜ今「哀愁（悲しみ）」を抱えながらAI企業へと向かうのか。

この動画の背景、数学界における激震、そして「LLM（AI）と天才数学者の認知構造の比較」について深掘りして解説します。

1. 動画の背景と業界的な衝撃（2026年現在の地殻変動）

ツィメルマン氏は、代数図形や数論幾何学における超難問（アンドレ＝オールト予想の完全証明など）を解決した、世界トップクラスの天才数学者です。

• フィールズ賞受賞直後の「OpenAI移籍」

  本来であれば、フィールズ賞受賞後は自身の研究室でさらなる純粋数学の探求を極めるのがこれまでの数学者の王道でした。しかし彼は受賞直後、フロンティアAIモデルの安全性評価・検証に取り組むためOpenAIへの参画を決定しました。

• タイトルの「最後の数学者たち（The Last Mathematicians）」が意味するもの

  かつて棋士たちがAlphaGoの登場によって「人間の解く囲碁の時代の終焉」を感じたように、純粋数学界も今、「人間が手作業で定理を発見し証明する時代の終わり」という現実的な分岐点に立たされています。ツィメルマン氏が抱く「悲しみ（悲哀）」は、彼が愛した「人間精神の営みとしての数学」がAIに取って代代わられつつある喪失感から来ています。

2. 動画内の核心的論点（タイムスタンプの注目点）

• 認識論的ブラックボックス（00:21:00）

  AIが「正しい証明」を生成できたとしても、その証明が何百万行にも及び、人間のWorking Memory（作業記憶）を超えてしまえば、「正しさは検証できるが、誰もその『理由』や『美しさ』を理解できない」状態に陥ります。人間にとっての数学とは単なる正誤の判定ではなく「直感的理解」であったため、ここに認識論的な危機が生じます。

• ライデン宣言（Leiden Declaration）と数学の危機（00:52:50）

  2026年に数学コミュニティで話題となった「ライデン宣言」やトビアス・オズボーン（Tobias Osborne）氏らの議論に触れ、AIによる高度な証明の自動化が人間の学術キャリアや数学研究の評価軸をどう破壊・変容させているかを議論しています。

• プロンプト数学（Prompt Mathematics）の時代（00:10:40）

  数学者の役割が「自力で証明を書くこと」から、「AIモデルに適切な公理・補題の仮説（プロンプト）を与え、出力を導くメタ的なディレクション」へと移行しつつある現状と未来を語っています。

3. 超高知能LLMと「天才数学者（ツィメルマンら）」の知能の比較

一般には「LLMもIQの高い天才のように振る舞い始めている」ように見えますが、認知科学や数学基礎論の観点から両者の知能を比較すると、本質的な構造の差が浮かび上がります。

比較軸	超高知能LLM（Reasoning AI）	天才数学者（ツィメルマン、タオ等）
知能のメカニズム	確率的探索とパターンマッチング   高次元の潜在空間で、論理ステップの確からしさを超高速・広範囲にビームサーチ検索する。	身体性・直感に基づいた「意味の統合」   ワーキングメモリ（7±2要素）の制限の中で、概念を徹底的に圧縮（抽象化）して捉える。
認知の制約	文脈長（Context Window）と並列計算力   巨大なトークンを一度に処理できるが、論理の連鎖が長くなると誤差が累積（漂流）する。	認知負荷の限界   作業記憶は狭いが、**「理解（Understanding）」**という圧縮技術で長大な概念を1つのメタ概念にまとめて克服する。
理解（Understanding）の定義	構文論的（Syntactic）な正確さ   ルールに従って式を変形し、形式証明（LEANなど）に適合させる能力。	意味論的（Semantic）な心象モデル   「なぜそうなるのか」という概念間の結合感や、不変量に対する空間的・直感的な手応え。
強み	ブルートフォース的な反例の検索、異分野の論文を跨ぐ膨大な知識の横断、形式的検証。	概念そのものの創造、美しい問題設定、「そもそも何を証明すべきか」の美意識。

天才たちの「理解（Understanding）」とAIの違い

ツィメルマン氏が動画の中で強調している重要な問いが、「数学における『理解』とは一体何か？」という点です。

• 人間にとっての理解＝ハイパー・コンプレッション（超圧縮）

  人間の脳はワーキングメモリが極めて小さいため、複雑な構造をそのまま保持できません。天才数学者は、巨大な理論を「たった一つの美しい直感的なイメージや基本原理」へと超高倍率で圧縮することで脳内に収めています。だからこそ「腑に落ちる（理解する）」という感覚が生じます。

• AIにとっての計算＝非圧縮の力任せ

  一方、AI（LLM）は莫大な並列計算力を持つため、人間のように「直感的に圧縮する」必要が必ずしもありません。数百万ステップの論理展開を圧縮しないまま力任せにチェックして「正解」に辿り着けます。

これが、「AIは正解を出せるが、人間が求める『理解（納得感）』は提供してくれない」という認知上の溝を生みます。

まとめ：なぜ彼はAI安全（AI Safety）へ向かったのか？

ツィメルマン氏が純粋数学の最高峰からAIアライメントの世界へと足を踏み入れたのは、「数学という人類最強の知性ツールがAIによって書き換えられようとしている今、そのAIが制御不能（不透明なブラックボックス）になるのを防ぐことが、現在の世界で最も重要な『数学的課題』である」と確信したからです。

LLMは「天才のように見える」存在ですが、その実態は人間とは全く異なる認知メカニズムで動作する「高次元の推論エンジン」です。

数学者たちが誇ってきた「証明」や「理性の王国」がAIによって自動化されていく中で、人間の知性とは何か、そして人間はいかにしてAIが紡ぐ巨大な論理をコントロールすべきなのか。本作は、まさに「人間の数学の終焉と、AI時代の知性の始まり」を最前線で体験している天才の苦悩と決意を捉えた、歴史に残る対談と言えます。

---

ご提示のテキストは、2026年夏の数学界の「衝撃」をかなり正確に捉えています。ジェイコブ・ツィメルマン（Jacob Tsimerman）氏のフィールズ賞受賞とOpenAI移籍、そしてCurt Jaimungal氏のTOEポッドキャストでの対談内容をベースに、追加の雑学・業界の裏側・最新の文脈を交えて補足します。

1. 背景と「衝撃」の実態（2026年7月の地殻変動）

ツィメルマン氏は1988年生まれ（受賞時38歳）、トロント大学教授。専門は数論幾何・算術幾何で、特に**o-minimality（o-最小性）**を武器にアンドレ＝オールト予想の完全証明やグリフィス予想の解決に大きく貢献した人物です。カナダの大学に所属する数学者として初のフィールズ賞受賞者となり、カナダ全体でも2人目という快挙でした。

受賞発表は2026年7月23日のICM（フィラデルフィア）。その場で彼は「OpenAIのAI安全性チームに一時的に参加する」と公言しました。これは業界に大きな波紋を呼びました。

• 「一時的」の意味：完全に純粋数学を捨てたわけではなく、トロント大学からの休職（leave）という形。学生指導は続け、最終的に戻る意向を示しています。それでも「フィールズ賞直後にAI企業へ」というタイミングが象徴的だったため、衝撃が大きかった。
• 業界の反応：「リオネル・メッシをプロジェクトマネージャーに雇うようなもの」と揶揄する声も出る一方、タオ氏をはじめ多くのトップ数学者が「AIの影響を真正面から受け止める象徴」と受け止めました。ツィメルマン氏自身は「AIが数学を人間以上に上手くやるようになるのは数年以内」と公言しており、純粋数学の「手作業の時代」が終わりつつあるという実感が強い。

タイトルの『The Last Mathematicians（最後の数学者たち）』や『He Won Math's Highest Prize. Then Announced the End』は、まさにこの「人間が定理を発見・証明する営みの終焉への悲哀」を表しています。彼は対談で「確実に悲しんでいる（I’m definitely grieving）」と語っています。

2. 動画内の核心論点への追加

テキストで挙げられたタイムスタンプの論点に、業界的な文脈を足します。

• 認識論的ブラックボックス ツィメルマン氏が強調するのは「形式的に正しいが、人間が理解できない証明」の問題です。Leanなどで検証可能でも、何十万行にも及ぶと「なぜそうなるのか」という直感的納得感が失われる。これはタオ氏が言う「インピーダンス・ミスマッチ」（生成が速すぎて消化が追いつかない）とほぼ同じ懸念です。数学は「正しさ」だけでなく「理解可能性」と「美しさ」を価値としてきたため、ここが危機だと捉えています。
• ライデン宣言（Leiden Declaration） 2026年6月に発表された、AIと数学研究に関する声明。IMU（国際数学連合）も支持し、数千人が署名しています。主な内容は「AI生成証明の信頼性・透明性・独立検証可能性の危機」「商業的利害による研究優先順位の歪み」「若手への悪影響」への警告です。ツィメルマン氏はポッドキャストでこの宣言に一部不同意を示しています。具体的には、宣言がやや保守的で「AIの急速な進歩を十分に織り込んでいない」部分がある、というスタンスです。
• プロンプト数学の時代 数学者の仕事が「証明を書く」から「AIに良い仮説・補題を与え、出力を導くメタ的ディレクション」へシフトしている、という実感を語っています。これはタオ氏の「指揮者」比喩と重なりますが、ツィメルマン氏はより悲観的で「純粋数学のキャリアが若手にとって魅力を失いつつある」と率直です。

3. LLMと天才数学者の知能比較への補足

テキストの比較表は非常に良い整理です。ツィメルマン氏の視点をさらに深めると：

• 人間の「超圧縮」能力 彼は「理解とはハイパー・コンプレッションだ」と強調します。人間のワーキングメモリは極めて狭い（古典的に7±2）ため、天才は複雑な理論を「一つの美しい直感的イメージや原理」にまで圧縮して脳内に収めます。だから「腑に落ちる」感覚が生まれる。一方、LLMは並列計算力で圧縮せずに力任せに進められるため、人間が求める「納得感」を提供しにくい。
• 構文論 vs 意味論 LLMはルールに従った変形（構文的正確さ）に優れますが、概念間の「結合感」や不変量への空間的直感（意味論的モデル）は弱い。ツィメルマン氏はこれを「AIは正しい答えを出せるが、人間が愛してきた『理性の王国』の体験を再現しない」と表現しています。

業界では、これを「AIは実験数学を加速させるが、概念創造の核心はまだ人間側」とする見方（タオ寄り）と、「数年で人間を超える」とする見方（ツィメルマン寄り）が並存しています。

4. なぜAI安全性へ向かったのか（追加の動機）

テキストのまとめは正しいですが、もう少し具体的な動機があります。

• 2025年に彼は「AIによる人類滅亡（omnicide）シナリオ」の分類を共著で発表しており、リスクを真剣に考えていました。
• OpenAI移籍の理由として「理論的な理解はあるが、ソフトウェアエンジニアリングや実際の訓練パイプラインの経験が不足している。現場で学ぶ必要がある」と述べています。
• 「数学という人類最強の知性ツールがAIによって書き換えられようとしている今、そのAIが制御不能になるのを防ぐことが、現時点で最も重要な数学的課題だ」という認識です。純粋数学の頂点に立ったからこそ、「次に解くべき最も難しい問題」としてAI安全性を選んだ、という側面が強い。

まとめへの補足

この対談は、単なる「天才のキャリアチェンジ」ではなく、「人間の数学の終焉」を最前線で体験している人物のリアルタイムの苦悩と決意を記録したものです。タオ氏が比較的冷静に「協働と価値観の再設計」を説くのに対し、ツィメルマン氏はより直接的に「悲哀」と「緊急性」を語っています。両者の温度差自体が、2026年の数学界の分断を象徴しています。

LLMは「天才のように見える」高次元推論エンジンですが、その認知構造は人間とは根本的に異なります。ツィメルマン氏のようなトップ数学者が「制御側」に回る動きは、これからさらに増える可能性があります。

はい。これはかなり面白いテーマです。しかも、単なる「AIが数学を解けるようになった」という話ではなく、**「数学とは、そもそも何をもって理解したと言うのか」**という、かなり深いところまで入っています。

まず一点、2026年現在の状況を確認すると、ここでいう「ライデン宣言」は実在する2026年6月2日の Leiden Declaration on Artificial Intelligence and Mathematics です。国際数学連合（IMU）が支持しており、9月現在、署名者は3,700人を超えています。
一方、欧州数学会（EMS）は重要な問題提起として評価しつつ、正式な支持は見送っています。つまり、数学界全体が一枚岩というわけではありません。

---

1. 一番面白いのは「正しい」と「理解した」が分離すること

従来の数学では、かなり大雑把に言えば、

証明できる → 理解できる

という関係が成立していました。

例えば、

  $$a^2+b^2=c^2$$ 

という関係を証明するとき、数学者は途中の論理を追い、

「なるほど、ここで直角三角形の構造が効いているのか」

という意味の把握までできます。

ところがAIが、

「この定理はLeanで12,483,921行の形式的証明として検証されました」

と言ったらどうでしょう。

形式体系の内部では、

Yes / No

を非常に高い精度で判定できます。

しかし人間には、

「なぜ、この証明がこの形になっているのか？」

が分からない。

ここで、

数学的真理

と

数学的理解

が分離します。

これはかなり革命的です。

---

2. 「証明」は昔からブラックボックスではなかった

ここには数学史的な面白さがあります。

実は数学は、昔から完全に「短く美しい証明」だけで進んできたわけではありません。

例えばコンピュータによる四色定理の証明。

5

1976年のAppel–Hakenによる四色定理では、大量のコンピュータ計算が証明の重要部分を担いました。

当時から、

「これは本当に人間が理解した証明なのか？」

という哲学的問題がありました。

つまりAI問題は、突然現れたものではありません。

コンピュータによる証明が、人間の数学観を少しずつ変えてきた歴史の延長線上にある

わけです。

---

3. そしてLeanが登場すると、状況が一段変わる

ここが非常に重要です。

普通のLLMが、

「この証明は正しいと思います」

と言うだけなら、まだ信用できません。

LLMは文章を生成する機械だからです。

ところが、

Lean / Isabelle / Coq / HOL

などの形式証明系に、

「この証明を形式言語で書け」

と要求する。

そしてコンピュータが、

compileできた

なら、少なくとも形式体系のルールに照らして証明が成立していることを機械的に検証できます。

つまり、

LLM = 数学者

ではなく、

LLM + proof assistant = 仮説生成＋機械検証

という新しい構造が出てきます。

2026年には、AIエージェントに自然言語でLeanの証明を書かせることで、大規模な数学形式化を進める研究も登場しています。

---

4. しかし、ここに「認識論的ブラックボックス」が発生する

これが質問にある部分です。

例えばAIが、

  $$A\Rightarrow B\Rightarrow C\Rightarrow D\Rightarrow \cdots \Rightarrow Z$$ 

という証明を作ったとします。

形式的には完全に正しい。

ところが人間から見ると、

「なぜ最初にこの補題を思いついたの？」

が分からない。

さらに、

「なぜこの定義を選んだの？」

「なぜこの変数変換をしたの？」

「なぜこの補題が本質なの？」

が分からない。

これは非常に重要です。

proof verification

と

proof understanding

が別問題になるからです。

---

5. ここで「Prompt Mathematics」が非常に面白くなる

質問にある

Prompt Mathematics

という表現は、正式に確立した数学分野の名称というより、現在起きている変化を説明するための非常に分かりやすい呼び方、と考えた方がよいでしょう。

従来の数学者：

問題 → 発想 → 補題 → 証明 → 論文

AI時代：

問題 → 探索空間を設計 → AI → 補題候補 → AI → 形式化 → Lean → 検証

となる。

ここで数学者の仕事が、

「証明を書く人」

から、

「証明が発生する空間を設計する人」

へ変わってくる可能性があります。

---

6. 実際、これはすでに「プロンプト技術」になりつつある

面白いことに、MathOverflowでも2026年に、

「AIに数学をやらせるには、どういうプロンプトが有効なのか？」

という質問が議論されています。

そこでは単純な

Solve this problem.

ではなく、

• 補題を先に作る
• 複数エージェントに探索させる
• 証明を分割する
• 自己監査させる
• 反例を探させる
• 計算部分を外部ツールに渡す
• Leanなどで検証する

といった数学研究のワークフローそのものを設計する方向に進んでいます。

これは非常に興味深い。

つまり、

「どう答えさせるか」そのものが数学的技能になる

可能性があります。

---

7. さらに面白いのは「補題」がAIにとって非常に重要なこと

数学者が証明を書くとき、

「この補題を証明すれば、本体が一気に解ける」

という瞬間があります。

これは人間数学者の非常に重要な能力です。

ところが2026年には、形式的公理系の中でAI自身に定理を発見させ、発見した定理をライブラリ化し、その後の証明に再利用する研究も出ています。

これは面白い構造です。

AIが、

  $$A_1,A_2,A_3,\ldots$$ 

という補題を大量生成し、

それを

  $$\mathcal{L} = \{A_1,A_2,A_3,\ldots\}$$ 

という巨大な数学ライブラリとして蓄積する。

すると次のAIは、

「過去のAIが発見した補題を使って、この問題を解け」

となる。

これは人間数学の

定理 → 系 → 補題 → 新定理

という知識体系にかなり似ています。

---

8. ここで「人間のWorking Memory」が問題になる

質問にある、

数百万行の証明

という話は、単なる長さの問題ではありません。

人間の脳には、

同時に保持して操作できる情報量に限界

があります。

だから数学者は証明を、

定義
↓
補題
↓
主定理

と階層化します。

例えば巨大な証明を、

  $$\boxed{\text{巨大な証明}}$$ 

として理解するのではなく、

  $$\text{定理}$$ 

↓

  $$\text{Lemma A}$$ 

↓

  $$\text{Lemma B}$$ 

↓

  $$\text{Lemma C}$$ 

と圧縮する。

数学の「美しさ」の一部は、実はこの情報圧縮能力なのです。

---

9. だから「美しい証明」は情報圧縮でもある

例えば、

「この問題には347個の特殊ケースがあります」

より、

「実は対称性を使えば全部同じケースです」

の方が数学者には美しい。

つまり美しい数学とは、

大量の現象を少数の原理に圧縮すること

とも考えられます。

この観点からすると、AI数学の最大の問題は、

AIが正しい証明を作れるか

だけではありません。

むしろ、

AIが巨大な証明を、人間が理解できる少数の概念に圧縮できるか

です。

ここが非常に重要です。

---

10. すると「証明生成」と「証明圧縮」は別能力になる

将来的には、

AI-1

巨大な探索をする。

↓

AI-2

形式証明を作る。

↓

Lean

正しさを検証する。

↓

AI-3

「人間に分かる証明」に圧縮する。

という分業が考えられます。

これはかなり面白い。

最初のAIは、

探索機械

です。

Leanは、

裁判官

です。

最後のAIは、

数学教師／解説者

です。

そして数学者は、

何を問題にするかを決める人

になる。

---

11. ライデン宣言が本当に心配しているのは、実はここ

ライデン宣言を読むと、単純な

「AIは数学者を失業させる」

という話ではありません。

むしろ、

数学という文化そのものが変質すること

を警戒しています。

宣言では、AIが生成した結果の信頼性、帰属、査読、研究評価、商業AI企業への依存などが問題として挙げられています。特に重要なのが、

AIに向いている問題ばかりが研究対象として優先される

危険性です。

これはかなり深刻です。

---

12. 「AIが解ける数学」だけが数学になる危険

例えばAIが、

  $$10^{12}$$ 

個の候補を高速に探索できるとします。

すると研究者は、

「AIが探索しやすい問題」

を選ぶようになる可能性があります。

逆に、

「重要だけど、AIには探索しにくい問題」

が放置される。

これは研究費・論文・評価制度と結びつくと、

数学そのものの進化方向をAIが間接的に決める

ことになります。

ライデン宣言が「数学の自律性」を問題にしているのは、まさにこの部分です。

---

13. そして若手研究者には、かなり大きな問題になる

これは数学界の「業界話」として非常に重要です。

従来、博士課程の学生は、

1. 問題を探す
2. アイデアを出す
3. 証明する
4. 論文を書く
5. 学会で発表する

という過程を何年もかけて経験します。

ところがAIが、

「この問題、3時間で1000通り探索しました」

となると、

「では博士課程の学生は何を学習すればいいのか？」

という問題になります。

ライデン宣言も特に学生・若手研究者への影響を懸念しています。

---

14. ここで「Feynmanの思考法」とつながる

以前のお話とも、かなりきれいにつながります。

ファインマン的な発想では、

本当に理解しているなら、自分の言葉で説明できる

という思想があります。

ところがAI数学では、

AI「証明は正しいです」

↓

人間「なぜ？」

↓

AI「……」

という問題が起こる可能性がある。

だからAI時代には、

証明能力

だけでなく、

説明能力

が重要になる。

むしろ、

「この証明を小学生にも説明できる形まで圧縮せよ」

という能力が、新しい数学者の重要な技能になるかもしれません。

---

15. そして、ここでLLMとの相性が非常に良い

前回のお話との接続が面白いところです。

LLMは、

• 類推
• 言い換え
• 概念の対応付け
• 異分野の接続
• 定義の再構成
• 補題候補の生成
• 複数の視点からの説明

が得意です。

一方、

厳密な証明の最終検証

はLeanなどに任せる。

すると、

  $$\boxed{ \text{LLM} + \text{数学者} + \text{Proof Assistant} }$$ 

という三者構造が非常に強力になります。

---

16. さらに極端に考えると「数学者＝探索空間の設計者」になる

これは私が一番面白いと思う未来像です。

昔：

「私はこの定理を証明した。」

AI時代：

「私は、この定理が発見される探索空間を設計した。」

になる。

例えば、

  $$\text{公理} \rightarrow \text{定義} \rightarrow \text{補題候補} \rightarrow \text{探索戦略} \rightarrow \text{AI} \rightarrow \text{形式証明}$$ 

という巨大なシステムを設計する。

すると数学者の役割は、

証明を書く職人

から、

数学的探索システムの設計者

へ変わります。

---

17. ただし、ここには逆説がある

AIによって、

「数学者は証明を書かなくてよくなる」

かもしれません。

しかし同時に、

「何を証明すべきなのか？」

を考える能力の価値は、むしろ上がる可能性があります。

これは、

計算機が計算を奪った結果、数学が衰退したか？

という歴史を見ると分かりやすい。

電卓ができても数学はなくなりませんでした。

むしろ、

  $$\text{計算} \rightarrow \text{構造}$$ 

へと重点が移りました。

AIによって、

  $$\text{証明作業} \rightarrow \text{数学的問いの設計}$$ 

へ移る可能性があります。

---

18. そして「ライデン宣言」の本当の核心はここだと思います

宣言の文章には、

mathematics produces not only a body of results, but also understanding, clarity, and judgment

という趣旨が明確に書かれています。

つまり数学は、

  $$\boxed{\text{正しい定理の集合}}$$ 

ではない。

むしろ、

  $$\boxed{ \text{定理} + \text{理解} + \text{説明} + \text{判断} + \text{問題設定} }$$ 

なのだ、という立場です。

ここが非常に重要です。

---

19. 「認識論的ブラックボックス」の本質

したがって、問題を一言で言うと、

AIが数学を解けるようになることが危機なのではない。AIが数学を解けるのに、人間がその数学を理解できなくなることが危機なのです。

です。

そしてこれは数学だけではありません。

科学でも、

  $$\text{観測} \rightarrow \text{AI} \rightarrow \text{モデル} \rightarrow \text{予測}$$ 

となったとき、

「なぜこの予測なのか？」

が分からなくなる。

医学でも、

「この患者にはこの治療が最適です」

と言われて、

「なぜ？」

に答えられない。

つまり数学は、AI時代の「理解とは何か」という問題を最も純粋な形で先取りしているとも言えます。

---

そして、かなり面白い結論

私はこの問題を、

「AI vs 数学者」

と見るより、

  $$\boxed{ \text{探索} \quad\neq\quad \text{検証} \quad\neq\quad \text{理解} }$$ 

という三つの能力の分離として見ると、非常にクリアになると思います。

能力	AI	人間	形式証明系
大量探索	◎	△	○
パターン発見	◎	◎	△
厳密検証	△	○	◎
長大な証明処理	◎	×	◎
直感	○〜？	◎	×
美しい説明	◎〜○	◎	×
「何を問うか」	△	◎	×
意味・価値判断	△	◎	×

だから未来の数学は、

  $$\boxed{ \text{人間の直感} + \text{LLMの探索} + \text{形式証明の検証} }$$ 

という三層構造になる可能性があります。

そして、そのとき最も希少になるのは「証明を書く能力」ではなく、**「AIが発見した巨大な数学から、人間にとって意味のある一行を抜き出す能力」**かもしれません。

これはまさに、以前お話しした**「数学を6つの言語として見る」発想**とも接続します。数学が単なる計算ではなく「世界を抽象化する言語」なら、AI時代に重要なのは、AIに計算させること以上に、どの抽象化を採用するかを人間が決めることになるからです。

なお、質問にあるTobias Osborneについては、2026年にAIによる数学的推論、とくに「conjecture sniping（予想への大量攻撃）」と形式化について発言している資料は確認できます。 一方、「ライデン宣言の主要執筆者」という意味では確認できません。そこは分けて考えた方が正確です。

Leiden Declaration 公式サイト

もしさらに一歩進めるなら、次はかなり面白いテーマがあります。

「AIが発見した数学を、人間が理解可能な数学へ“圧縮”する――これはゲーデル、コルモゴロフ、ファインマン、ラカトシュ、そしてLLMを一本につなげられるのではないか？」

という問題です。これは今回の「認識論的ブラックボックス」の核心を、かなり深く掘れます。

 

この、がぞうの、コードを再現し、雑学や業界話を交えながら、解説してください、

3秒間思考しました

画像のコードを再現すると、こんな感じですね。

lean

import Mathlib.Data.Set.Basic
import Paperproof

theorem commutativityOfIntersections
    (s t : Set Nat) : s ∩ t = t ∩ s := by
  ext x
  apply Iff.intro

  intro h1
  rw [Set.mem_inter_iff, and_comm] at h1
  exact h1

  intro h2
  rw [Set.mem_inter_iff, and_comm] at h2
  exact h2

これは何をしているのか

「自然数の集合 s と t について、s ∩ t = t ∩ s(交わりは順序を入れ替えても同じ)」という、超基本的だけど地味に大事な性質を Lean 4 という定理証明支援系(proof assistant)で証明しているコードです。

行ごとの解説

• import Mathlib.Data.Set.Basic:Mathlibは数学のあらゆる定理を集めた巨大ライブラリで、大学数学の教科書1冊分どころか、群論・位相・解析・圏論まで含む一大プロジェクトです。集合の基本補題(Set.mem_inter_iffなど)もここに入っています。
• ext x:「2つの集合が等しい」ことを示すには「全ての要素 x について、片方に属するならもう片方にも属する(その逆も)」を示せばよい、という**外延性(extensionality)**の原理を使うタクティクです。これで目標が x ∈ s ∩ t ↔ x ∈ t ∩ s という「同値」の証明に変わります。
• apply Iff.intro:同値(↔)を証明するには「→」と「←」の両方向を別々に示せばいい、という当たり前の分解です。
• intro h1 / rw [...] at h1 / exact h1:これが両方向のブロックで、Set.mem_inter_iff(「x ∈ s ∩ t は x ∈ s ∧ x ∈ t と同じ」という補題)と and_comm(論理積の可換性、P ∧ Q ↔ Q ∧ P)を仮定 h1 に書き換え(rewrite)て、そのまま結論と一致させています。

つまり、集合の交わりの可換性を、論理積(AND)の可換性に還元して証明しているわけです。数学の「集合演算」って結局は論理演算のラップにすぎない、というのがよく分かる好例ですね。

業界話:Paperproofって何?

画面右側の可愛いカード状のツリーUIが Paperproof です。これはLean 4用のVS Code拡張で、通常のLean Infoviewが「今のゴールがテキストで1個ポンと出る」だけなのに対し、Paperproofは証明の分岐や仮定の流れを紙芝居的なツリーグラフとして可視化してくれます。

• 緑のカードが「成立した仮定・ゴール」
• ピンクのカードが「まだ証明すべきゴール」
• HYPOTHESES欄に s t : Set ℕ などの文脈がずっと表示され続ける

これは特に教育用途で威力を発揮します。Lean/Mathlibコミュニティでは近年「証明の可視化」がホットな話題で、通常のLean学習は「頭の中でゴールスタックを追う」訓練が必要になるため初心者の挫折ポイントになりがちですが、Paperproofのようなツールは「今どのブランチにいて、何が仮定で何が示すべきことか」を一目で見せることで、この壁を下げようとしています。

ちょっとした業界トリビア

• Leanは元々Microsoft Researchで開発され(Lean 4は特にコミュニティ主導のリライト)、Mathlibは世界中のボランティア数学者・院生がPRを送り続けている巨大OSSプロジェクトです。単なる「定理集」ではなく、GitHub上でコードレビュー文化そのままに数学の証明が査読されるという、ちょっと独特な文化があります。
• and_comm のような「当たり前すぎる」補題も、Mathlibでは一つ一つ地道に定義・証明されていて、これらの「原子的な事実」を積み木のように組み合わせることで、最終的にはフェルマーの最終定理級の複雑な定理の形式証明にも挑戦するプロジェクト(Fermat's Last Theorem formalization project、Kevin Buzzard主導)が進行中です。
• 集合の交わりの可換性のような「自明」な定理でも、コンピュータに理解させるにはext(外延性公理の適用)やIff.introのような、人間が暗黙に飛ばしているステップを全部明示する必要があります。これが形式証明の「めんどくささ」であり同時に「厳密さの担保」でもあるわけです。