# 数学は永遠に変わった — Kevin Hartnett『The Proof in the Code』とLeanの物語

- 番組: [Machine Learning Street Talk (MLST)](https://ai-curator.jp/podcasts/shows/cmv3z5bzn00075o10ok1p46w3)（Machine Learning Street Talk (MLST)）
- 元のタイトル: Mathematics Just Changed Forever — Kevin Hartnett
- 配信日: 2026年10月26日
- 長さ: 1時間33分
- 要約作成日: 2026年10月27日
- トピック: [#Lean](https://ai-curator.jp/topics/Lean) [#定理証明支援系](https://ai-curator.jp/topics/%E5%AE%9A%E7%90%86%E8%A8%BC%E6%98%8E%E6%94%AF%E6%8F%B4%E7%B3%BB) [#形式検証](https://ai-curator.jp/topics/%E5%BD%A2%E5%BC%8F%E6%A4%9C%E8%A8%BC) [#AlphaProof](https://ai-curator.jp/topics/AlphaProof) [#自動形式化](https://ai-curator.jp/topics/%E8%87%AA%E5%8B%95%E5%BD%A2%E5%BC%8F%E5%8C%96) [#AI数学](https://ai-curator.jp/topics/AI%E6%95%B0%E5%AD%A6)
- URL: https://ai-curator.jp/podcasts/cmvpefdg100014f10z5yuwtnv

## 要約

Kevin Hartnett の著書『The Proof in the Code』を軸に、証明支援系 Lean の誕生から数学界での普及、そして AI 数学までをたどるドキュメンタリー回。ケプラー予想の証明を検証できなかった問題に始まり、Leo de Moura、Kevin Buzzard らの物語が語られる。後半では AlphaProof や自動形式化を通じて、機械が出した証明で何が検証されたのかという「形式化ギャップ」が論じられる。

## ポイント

- Thomas Hales のケプラー予想の証明は計算機コードに大きく依存し、Annals of Mathematics は査読で真偽を判断できず、「99%確信」という注記付きで受理されたと語られる。
- Lean の信頼は小さなカーネルだけに置かれる設計で、偽の命題を真と認める誤りが最大の罪とされる。Leo de Moura は Z3 から対話型定理証明器へ進んだ。
- Jeremy Avigad の働きかけで Lean は依存型理論を採用し、Mathlib が数学者の協働でバーンレイジングのように育ち、Lean の数学利用が広がった。
- Kevin Buzzard らは Annals 掲載の定理50件を形式化する過程で、論文の記述自体が厳密には誤りだった例を AI が見つけたと述べる。
- AI が生む Lean コードは Mathlib の「適切な抽象化」の理念と衝突しうる。出力が検証済みでも、形式化された命題が人間の意図を捉えているかという信頼の問題は残る。
- Lean 検証済みの zlib 実装の例から、部分的な仕様では報酬ハッキングが起こりうるという指摘がなされ、AI 時代のソフトウェア検証の課題が示される。

## 章立て

- [01:48] **ケプラー予想と検証不能な証明** — Hales のコード依存の証明が Annals で検証できなかった経緯と、数学者が証明を信頼する社会的プロセスを紹介する。
- [09:04] **正しさと有用さの違い** — AI の証明は Hales の証明のように読みにくいという指摘と、新しい概念を生むことが数学の価値だという議論、形式化への抵抗。
- [12:53] **Lean と小さなカーネル、Z3 から Lean へ** — Lean の概要、信頼するのはカーネルのみという設計思想、Microsoft での Z3 開発から対話型証明器への移行。
- [18:42] **基礎をめぐる議論と Buzzard の危機感** — 依存型理論の採用をめぐる Avigad と de Moura のやり取り、ユーザー増加による負担、Buzzard が数学を「トランプの家」と懸念した話。
- [30:43] **Mathlib とペルフェクトイド空間** — Mathlib の成り立ち、スキームやペルフェクトイド空間の形式化、Scholze の Liquid Tensor 検証の経緯。
- [53:20] **AI と数学：AlphaProof から Tao の実験まで** — AlphaProof による IMO 銀メダル水準、自動形式化、Tao の Equational Theories プロジェクト、自然言語証明の登場。
- [1:03:16] **形式化ギャップと理解の問題** — AI 生成 Lean コードと Mathlib の理念、検証済みでも誤った対象を証明しうる問題、論文の誤りを見つけた話。
- [1:16:58] **zlib の例と Lean を巡る人間ドラマ** — 仕様の不完全さと報酬ハッキング、AI 時代の検証、de Moura と数学者たちの対立と和解を語る。

## 解説記事

数学の証明を機械で検証する時代が来た。今回の Machine Learning Street Talk は、Kevin Hartnett の著書『The Proof in the Code』を軸にしたドキュメンタリー形式の回である。Hartnett に加え、Lean の生みの親 Leo de Moura、Jeremy Avigad、Kevin Buzzard らが登場し、Lean が数学界で受け入れられていく過程と、AI 時代に何が検証されたといえるのかという問いを扱う。

#### ケプラー予想と「確かめられない証明」

物語は Thomas Hales によるケプラー予想（球の最密充填）の証明から始まる。Hales は問題を約1,700通りの配置に帰着させ、それぞれを計算機プログラムで検証した。ところが提出先の Annals of Mathematics は、この証明をどう査読すべきか分からず、長年結論が出なかったと語られる。最終的に論文は「99%確信」という注記付きで受理されたという。

ここで示されるのは、数学者が証明を信じる過程が実は社会的なものだという点だ。誰が書いたか、既存の知識にどれだけ近いかを頼りに、すべての行を確かめないまま信頼している。Hales はその後、HOL Light や Isabelle といった証明支援系で自身の証明を形式化した。投じた労力は約20人年に及ぶとされ、得られたのは正しさの保証だけだった。数学者が形式化に冷淡だった理由として、De Bruijn 比（形式化に必要なコード量と非形式の数学の比。20対1あるいはそれ以上）の高さが挙げられる。

#### Lean の設計：小さなカーネルと依存型理論

Lean はプログラミング言語であり証明支援系でもある。信頼を置く対象は「カーネル」と呼ばれる小さな検査プログラムだけで、周辺に多少のバグがあっても結果の信頼性は保たれるという。カーネルにとって最大の罪は、偽の命題を真と認めてしまうことだと説明される。

de Moura は Microsoft で自動定理証明器 Z3 を作り、ソフトウェアのバグ検出で成果を上げ、競技会でも優勝した。その後、より表現力の高い対話型定理証明器へ向かう。当初 de Moura は単純な基礎理論を志向したが、抽象代数を扱いたい Avigad の主張を受け、2013年に依存型理論の採用を決めた。後の Mathlib がサイバーセキュリティ（暗号）の検証にも適した抽象化を備えていたという証言も紹介される。一方、ユーザーが急増して要望に追われた de Moura が苛立ち、のちに距離を置いた経緯も描かれる。

#### Mathlib と数学者たち

Buzzard は、後続論文に不備や論理の飛躍を見つけ、自分の分野が「トランプの家」になりかねないと感じたことが Lean に関わる動機だったと述べる。Mathlib は中央の権威なしに育ったコミュニティ主導のライブラリで、Hartnett は「バーンレイジング（共同作業）の精神」と形容する。Buzzard は複素数を実装し、学部生に形式化を手伝わせた。

転機は Peter Scholze からの依頼だった。Scholze は自分の論文の定理の証明が実際に読まれているか不安を抱いていた。Buzzard らは約半年で検証を終え、「機械が正しいと言った」と報告し、証明の概念的な簡略化も得られたという。この成果が広く注目を集め、Lean への関心が一気に高まった。

#### AI 数学と形式化ギャップ

後半は AI の話題である。DeepMind の AlphaProof は2024年の IMO で銀メダル水準に達し、Lean の証明を出力して検証した。そのために数千万規模の問題を Lean へ自動形式化したとされる。2025年7月には自然言語の証明で金メダル水準の報告もあり、Lean を使わない道も現れた。Tao の Equational Theories プロジェクトは、大規模協働と Lean による検証で「実験数学」の可能性を示した。

Buzzard は、AI が人間の本を機械的に Lean に訳すことで、Mathlib が重視してきた「正しい抽象化」の意義が揺らぐと語る。Hartnett は、自動形式化の産物が Mathlib の基準に合わないことを「トロイの木馬」と表現した。

核心は「形式化ギャップ」である。検査器が保証するのは導出の正しさで、形式化された命題が人間の意図を捉えているかは保証しない。Buzzard のチームが Annals の定理50件の形式化を AI にチェックさせたところ、論文の記述が厳密には偽だった例が見つかり、4人のフィールズ賞受賞者の論文も含まれていたという。機械は人間の「99%の精度」を100%に引き上げる役割を果たす、と彼は述べる。

zlib の例も示された。AI が Lean で圧縮・展開の実装を作り、往復で元に戻る性質を証明したが、性質の指定が不十分だと恒等関数のような自明な実装でも満たされてしまう。仕様が全体を覆っているかが課題で、AI に任せきりにするほど重要になると語られる。

#### まとめ

本回は、形式検証が「証明の正しさ」を保証する一方、「何を証明するか」という人間の判断が最後まで残ることを示した。AI がコードや証明を大量に出す時代には、仕様や定義の妥当性をどう担保するかが焦点になる。日本のエンジニアや研究者にとっても、AI 生成物の検証と仕様設計は他人事ではない。Lean や Mathlib の動向に加え、人間が理解と意図をどう保つかという議論に注目したい。

> この要約・解説記事は、元の音声の文字起こしをもとに AI（Claude）が日本語で作成したものです。出典: Machine Learning Street Talk (MLST)「Mathematics Just Changed Forever — Kevin Hartnett」