Machine Learning Street Talk (MLST)
人間が読めない証明を誰が検証するのか — Leonardo de Moura（Lean 創始者）
Who Checks a Proof No Human Can Read? — Leo de Moura
Lean と Z3 の生みの親 Leonardo de Moura が、Lean の中核を小さく保つ「カテドラル型」運営の理由と、コラッツ予想の「反証」を受理してしまった事件について語った回。公式カーネルと外部チェッカー Nanoda がそれぞれ別のバグを突かれた経緯を説明し、複数カーネルや検証済みカーネルで信頼の範囲を縮める方針を述べている。後半は AI による zlib の検証、Mathlib の成長、AI の創造性の限界、Lean の今後と学習法に及ぶ。