https://www.youtube.com/watch?v=KzdYKeAqWhY

题目：《Lean 创始人访谈全记录：当形式化验证遇上 AI，手写数学与软件验证将如何被重塑》

第（一）部分 开场与核心命题：从“测试只能证明有 bug”到“证明可确保无 bug” （0% - 8%）

Dijkstra 名言引出形式化验证的根本价值：主持人以 Dijkstra 的名言“程序测试可用于揭示 bug 的存在，但永远无法证明 bug 的不存在”开场，指出 Lean 与形式化证明的意义恰恰在于“证明 bug 不可能发生”。

Lean 的基础定位：Lean 既是一门编程语言（可以写代码），也是一个证明系统（可以对代码写性质并用机器可检查的证明来验证）。它提供绝对正确的保证，并拥有多个独立的检查器。