AI 的數學證明靠 Lean 檢查，那誰來檢查 Lean？｜Leonardo de Moura｜演講訪談系列

00:00 開場：AI 的數學證明靠 Lean 檢查，那誰來檢查 Lean？ 00:59 Leonardo de Moura（Lean）：Lean 是什麼，數學的裁判 01:44 小而可信的核心：只需要相信幾千行 02:44 Collatz 假證明：兩套檢查程式都蓋了章 03:48 兩個不同的漏洞，被同一份證明對準 05:23 幾小時內修補，以及「這會一再發生」 06:25 訪談之後：OpenAI 內部模型又找到好幾個漏洞 07:32 把要相信的東西縮到最小：多位獨立裁判 09:35 Claude 把 zlib 翻成 Lean，證明壓縮再解壓不會出錯 10:44 證不出來就不准合併：只能往前的棘輪 11:56 章只蓋在寫下來的規格上：模糊測試找到的漏洞 13:44 120 萬行的證明：沒人讀得完，靠機器能檢查的證書 14:45 人剩下的工作：把規格寫對 大家好，我是 Jim，這裡是 AI Notebook。這一集是演講訪談系列，主角是 Leonardo de Moura，他是 Lean 的創造者，現在是 Lean FRO 的首席架構師。今年七月二十五號，網路上出現一份證明，說它推翻了一個放了將近九十年的數學猜想，叫 Collatz 猜想。這份證明附上了 Lean 的檢查結果，Lean 蓋了章。另一套獨立寫成的檢查程式，也蓋了章。可是這份證明是錯的。Collatz 猜想到今天，沒有人證明，也沒有人推翻。頻道前一支影片，我們講 OpenAI 公開七百多篇 AI 數學論文，那支片的結論之一是，附上 Lean 證明的成果，比較讓人放心。這一集要往下多問一層。連幫數學證明蓋章的程式都可能被騙，AI 大量交出證明以後，我們到底能相信什麼？這一集就只問這個問題。我們分三步看。先看蓋章的程式是怎麼被騙的，再看就算章是真的，它到底保證了什麼，最後看，當證明長到沒有人讀得完，人還剩下什麼工作。 原聲與訪談畫面片段取自 Machine Learning Street Talk 的訪談（下方第一個連結），版權屬原作者；本片為評論與教育用途的解說。訪談錄於 2026 年 7 月底、9 月底上架，片中「訪談之後」的事件（7 月底到 8 月的漏洞回報與修補）取自 Lean 團隊公開的事後報告。Collatz 猜想到現在仍然沒有被證明，也沒有被推翻；那份「推翻」它的證明是無效的。 📎 資料來源 • The Programming Language That Referees Mathematics – Leo de Moura（Machine Learning Street Talk，2026-09-29） https://youtu.be/ZpQFebTK75A • Leonardo de Moura：Postmortem for kernel soundness bug #14576（2026-08-01） https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/ • Leonardo de Moura：Postmortem for the kernel soundness bug hunt（2026-08-24） https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/ • Lean 4 Issue #14576（漏洞回報） https://github.com/leanprover/lean4/issues/14576 • Lean 4 PR #14577（修正） https://github.com/leanprover/lean4/pull/14577 • oss-security 公告：Lean kernel soundness bug（2026-08-02） https://openwall.com/lists/oss-security/2026/08/02/1 • CollatzLean（宣稱推翻 Collatz 猜想的 Lean 證明） https://github.com/xrchz/CollatzLean • nanoda_lib PR #22：more struct and inductive checks https://github.com/ammkrn/nanoda_lib/pull/22 • comparator（Lean 證明重新檢查工具） https://github.com/leanprover/comparator • Lean4Lean（Mario Carneiro） https://github.com/digama0/lean4lean • Leonardo de Moura：When AI Writes the World's Software, Who Verifies It?（2026-02-28） https://leodemoura.github.io/blog/2026-2-28-when-ai-writes-the-worlds-software-who-verifies-it/ • lean-zip（Kim Morrison） https://github.com/kim-em/lean-zip • Kim Morrison：Why Lean is faster than Rust（2026-07-24） https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-than-rust/ • Kiran Gopinathan：Who watches the watchers（lean-zip 模糊測試） https://kirancodes.me/posts/log-who-watches-the-watchers.html • Erdos90：OpenAI's 2026 counterexample to the Erdős unit distance conjecture（Lean 證明） https://github.com/plby/Erdos90 • Erdős Problems #90 https://www.erdosproblems.com/90 • Lean FRO：About https://lean-lang.org/fro/about/ --- Jim AI Notebook | Note the Future 每日深度解析 AI 最新進展 #LeonardodeMoura #Lean #LeanFRO #形式化證明 #Collatz猜想 #數學證明 #AI數學 #zlib #MachineLearningStreetTalk #演講訪談系列 #JimAINotebook