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

题目：《Lean 创始人访谈全记录：当形式化验证遇上 AI，手写数学与软件验证将如何被重塑》 第（一）部分 开场与核心命题：从“测试只能证明有 bug”到“证明可确保无 bug” （0% - 8%） - Dijkstra 名言引出形式化验证的根本价值：主持人以 Dijkstra 的名言“程序测试可用于揭示 bug 的存在，但永远无法证明 bug 的不存在”开场，指出 Lean 与形式化证明的意义恰恰在于“证明 bug 不可能发生”。 - Lean 的基础定位：Lean 既是一门编程语言（可以写代码），也是一个证明系统（可以对代码写性质并用机器可检查的证明来验证）。它提供绝对正确的保证，并拥有多个独立的检查器。 - Lean 应被视为平台：用户可以在 Lean 上写代码、写关于代码的性质命题、并给出证明；本期节目将围绕它如何工作、以及它如何改变数学和软件验证的未来展开，并提出“手写数学是否会终结”这一核心疑问。 第（二）部分 Lean 是什么：编程语言与证明助手的一体两面 （8% - 18%） - Lean 的双重身份：Lean 不仅可用于数学证明，也可用于软件验证。基于依赖类型论（Dependent Type Theory）的一族证明助手（如 Rocq/Coq 和 Lean）天然就是“编程语言 + 证明助手”。 - 软件验证的两种主流路径： • 浅嵌入（Shallow Embedding）：通过工具（如把 Rust 翻译到 Lean 的工具）把其他语言映射到 Lean 中进行验证。 • 深嵌入/语义建模：在 Lean 中为 C 语言等编写语义，把 C 程序表示为 Lean 中的数据结构，从而对其陈述性质并进行推理。 - 具体例子--数组越界验证：以 C 语言访问数组为例，可在 Lean 中把“索引 i 满足 0 ≤ i y”的证明--这意味着如果不提供该证明，就根本无法构造出这个结构的实例，不变量被天然植入语言。 • 在数学对象操作上，Lean 可把“群/环/域”等结构作为一等公民传递，而 HOL 要做同样的事需丑陋的编码技巧；主流数学家一致认为严肃数学必须用依赖类型论。 第（十一部分 Lean 的未来路线：发力软件验证与编程语言的身份 （86% - 93%） - Lean 非营利基金会与 AWS 的支持：Lean 已有 13 年历史，前 10 年是学术项目；2023 年成立的非营利基金会让它真正成为“产品”，AWS 提供了迄今最大笔捐赠，目标是加速 Lean 作为“可编程的软件验证系统”这条相对未被充分投入的路线。 - 数学验证与软件验证的差异：数学中“命题小、证明深”；软件中“命题大、证明浅（但对象庞大）”。未来重点是把 Lean 推向软件验证的极限。 - “证明带来的免费优化”：当 AI 告诉你“我优化了代码，这是行为等价的证明”时，软件优化不再是冒险，而是可放心交付的常态。这将是行业游戏规则的改变者。 - 学习 Lean 的建议：Lean 官网提供《Functional Programming in Lean》《Theorem Proving in Lean》《Mathematics in Lean》《The Mechanics of Proof》等书籍；但当今最高效的学习方式是开着 AI 智能体与 Lean 并肩工作--左边代码、右边 Info View、下边 AI 智能体用自然语言解释并写代码，背景不同（如懂 Haskell）还可让智能体定制教学。 第（十二）部分 收尾：给过去自己的建议与节目尾声 （93% - 100%） - 如果能回到构建 Z3/Lean 之初：嘉宾笑称“无知是福”，不会剧透具体的技术秘密；但如果一定要给当年的自己一句忠告，会是--好好锻炼人际交往能力。作为极度内向的人，他事后意识到与社区、用户的有效互动对项目成功至关重要。 - 致谢与呼吁：主持人对嘉宾表示感谢。 - 节目运营与周边：主持人呼吁观众点赞、评论、推荐下期嘉宾（此前 Barbara Liskov、Mike Stonebraker、Mark Brooker 等嘉宾均来自观众留言推荐）。 - 主持人个人项目广告：提到自己设计的分体工学分体键盘已在 Kickstarter 上线，8 小时达成目标，现开放 late pledge 预订链接。 Top comments (0)