Lean形式化验证创始人访谈：证明bug不存在而非仅发现

第（一）部分 开场与核心命题：从“测试只能证明有 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 < 10”写成数学命题；原来的 C 源文件可对应一份“元数据式”的 Lean 证明，由 Lean 逐行检查。

自动化与可维护性：人们会建立自动化框架（如基于前置条件-语句-后置条件的三元组），把证明过程变得更易管理；复杂度是软件验证的大敌，而 AI 的出现让“自动证明”成为可能，但前提是把证明写得模块化以便扩展。

第（三）部分 从“测试套件”到“形式化规格”：为什么规格优于测试（18% - 28%）

测试 vs. 证明的本质差异：测试套件再全面，也只覆盖了有限场景，角落案例仍可能遗漏；而形式化证明覆盖所有可能情况，真正做到了“bug 的不存在”。

Zlib 压缩库的震撼案例：主持人的同事 Kim Morrison 发起项目，让 AI 把 C 写的 Zlib 压缩库翻译进 Lean，要求通过原测试套件，并证明“压缩后再解压得到原始数据”这一强性质。结果仅用一周就完成了整个形式化，目前只需再做性能优化，且优化不能破坏既有证明。

规格说明（Specification）的成本讨论：写出一份好的规格，工作量因程序而异。一个实用技巧是：先用“低效但正确”的实现作为规格（Spec），再让 AI 生成高效版本并证明其与规格等价。

Jane Street 与工业界实践：Jane Street 等公司已在投资形式化验证，例如对微内核 seL4 的完整验证。过去这类工作在没有 AI 时“手动证明 + 维护证明”的成本极高（往往是写程序本身的 10 倍），而 AI 正在消除这种痛苦——AI 非常擅长撰写和维护形式化证明，即使人已经忘了当初为何这么证。

第（四）部分 Lean 作为编程语言的工程实践与工具链（28% - 36%）

不仅是证明助手，更是生产级编程语言：AWS 内部有一个约 50 万行 Lean 写的 AI 加速器编译器，主要把 Lean 当编程语言用，顺带获得一些性质证明作为“额外红利”。

工具链体验接近现代语言：构建系统 Lake 相当于 Rust 的 Cargo；编辑器用 VS Code，提供 IntelliSense 等熟悉体验。

Info View——Lean 独有的核心交互界面：屏幕通常一分为二，左侧是代码/证明文件，右侧 Info View 实时显示当前证明目标的状态变化，给用户持续反馈。

Tactic 模式：把证明当成“游戏”：用户通过 by 进入领域特定语言（DSL）来写证明，每一步可简化目标、应用已知引理等，看着目标逐步减少直到归零，过程极具“通关”快感，不少用户戏称自己“沉迷其中”。

第（五）部分 内核信任问题：Lean 自身是否被 Lean 验证？（36% - 42%）

只需信任极小的内核：Lean 整体庞大且规格频繁变动（如简化器的行为不断被用户定制），难以对全部进行形式化；但证明检查的核心——“内核”是可以被规格化的。

多内核策略确保可信：Lean 自带的内核并未被验证，但 Mario Carneiro 用 Lean 实现了名为“Lean for Lean”的内核，并证明了它与 Lean 语义的一致性。此外还有用 Rust 等语言实现的其他第三方内核。

内核的本质是类型检查：导出的 Lean 开发产物是一团二进制 blob，内核读取后做类型检查——确认所声称的定理（如“两偶数之和为偶数”）的类型与给出的证明项类型匹配。

内核应当短小精悍：高性能内核大约 5000 行代码，理想情况下任何人都能自己重写一个；外部内核还可打印出已证定理及其全部依赖，防止被误导。

第（六）部分 Lean 在数学形式化中的突破：IMO 金牌与重大猜想（42% - 52%）

IMO 金牌曾被认为不可能：几年前 AI 在国际数学奥林匹克（IMO）拿金牌被认为是天方夜谭，如今却成了“基准 easy 题”；DeepMind 的 AlphaProof 2024 年拿到银牌，初创公司 Harmonic、字节跳动等也相继拿下金牌。

单元距离猜想（Unit Distance Conjecture）的形式化：OpenAI 先给出了非形式的证明；Kim Morrison 把它作为挑战放到 Lean 的“量化形式化”挑战平台上；OpenAI 的 Boris Kusolovic 接下挑战，在 Lean 中给出了约 100 万行的完整形式化证明，从 OpenAI 放出证明到 Lean 中完成形式化，仅用了不到两周。

Lean 在数学界的崛起时间线：

• 2017 年启动“Lean 数学库（mathlib）”项目，Lean 首先在数学界流行。
• 2020 年初“液体张量实验（Liquid Tensor Experiment）”验证了菲尔兹奖得主舒尔茨（Scholze）的一项重要结果；当时他对自己未发表的结果没把握，而形式化团队在并未完全理解证明的情况下，借助 Info View 一步步引导，最终不仅完成了形式化，还简化了证明。
• 此后陶哲轩（Terence Tao）也开始使用 Lean，第一次觉得不会再用了，结果一周后又用 Lean 做了新成果，彻底“上瘾”。

“上瘾”的根源：Info View 的即时反馈让证明像解谜游戏；IMO 奖牌级的问题解决者尤其热爱这种“连续通关”的快感。Lean 开发者自己在开发中写证明也容易上头。

AI 如何玩转 Lean 证明游戏：AI 把 Lean 证明视为单人对战游戏，通过强化学习不断应用 tactic 步骤，观察 Info View 中目标状态的变化，直到“无目标残留（no goals left）”。mathlib 的丰富积累让 IMO 题目能被方便地翻译成 Lean 语句。

第（七）部分 AI + Lean 的边界：能发现新证明，但是否能创造新数学？（52% - 58%）

目前证据：AI 可发现新证明，但尚未创造新数学理论：AI 能在 Lean 环境下找到新的证明路径，甚至构造反例推翻猜想（那 100 万行证明中包含了显示某猜想为假的形式化证明）；但在“提出全新数学概念/理论”方面，目前仍看不到证据。

何时应投入形式化：当系统涉及安全关键（safety-critical）、或人本身对某个主题理解不够透彻时，形式化是极佳选择——几乎每位把算法形式化过的人都会感慨“形式化之后我才真正懂了它”。

形式化让人更敢做激进优化：有了性质证明保底，工程师不再害怕为了性能而改写代码，因为 AI 可以证明改写前后行为等价，或找出反例。

第（八）部分 展望未来：3-5 年内形式化验证与“手写数学”的命运（58% - 66%）

大模型训练才刚刚开始：各大实验室认真把 Lean 形式化验证纳入强化学习管线也是近一两年的事，当前已有的惊人表现未来还会大幅提升；成本将持续下降。

函数式语言借势主流化：Lean、Rocq 这类函数式语言会因为 AI 写代码、人只管规格而变得更加主流——人不再关心代码怎么写，只关心规格层。

“手写数学会终结吗？”——混合而非取代：总会有人像手工打造家具的匠人一样，愿意把证明雕琢成易于人类沟通的艺术品；但完全不用 AI 的数学家会非常罕见。未来是人机混合工作流：AI 承担重复性、无创造性的修补工作，人类负责提出规格与意图。

人类不会被淘汰的根本原因：AI 即便能自生数学，若无与人类世界的接口（规格说明）也无意义；人类永远在闭环中扮演“提出我们想要什么”的角色，同时人们依然享受写原型代码的乐趣（痛苦的是把原型变成产品，这部分可由 AI 接管）。

第（九）部分 Z3 SMT 求解器：Lean 的前身与互补技术（66% - 76%）

Z3 是什么：主持人提到嘉宾早年在微软研究院主导的 Z3，是一个 SMT（Satisfiability Modulo Theories）求解器；相比只能处理布尔逻辑的 SAT 求解器，Z3 支持算术、数组等背景理论。

Z3 与 Lean 的本质区别：

• Z3 是完全自动化的“按钮式”约束求解器，不是编程语言；Lean 是交互式证明助手（也带有自动化），同时也是编程语言。

Z3 的典型应用：

• 数独求解：把数独编码为约束，Z3 瞬间给出解。
• Bug 查找：将代码中某条疑似有安全漏洞的路径转化为约束送给 Z3；若返回“可满足”，则给出一个能触发该路径的具体输入；若“不可满足”，则说明该路径不可达。

为什么又造了 Lean：Z3 在“找 bug”上很成功，但在“证明 bug 不存在”上并不成功——当程序性质涉及到大量全称量词时，Z3 的启发式算法经常失败或超时，且对问题的微小改动可能导致证明不稳定。Lean 的诞生正是为了填补“交互式、可分解步骤、人类/AI 可控”的这一鸿沟。

Lean 更高效的关键：在 Z3 中用户只有“求解”这一个黑盒步骤；而在 Lean 中可以把证明拆成极其细致的逐步 tactic，人类和 AI 都能逐步说服检查器。

构建 Z3 与 Lean 的技术挑战：

• Lean 比 Z3 难一个数量级：Z3 面向的是懂自动推理的后端工具用户，接口简单（SMT-LIB 低级语言，输入输出 yes/no 或反例）；而 Lean 要服务数学家和程序员两类完全不同背景的用户，需要提供编程语言、库、LSP、构建系统、交互 UI 等一整套庞杂设施。
• Lean 自举（Bootstrapping）之痛：Lean 最初用 C++ 写，后来要把它自己用 Lean 重写。团队把功能精简到极致，用约 10 万行 Lean 代码自举；编译过程痛苦到“想哭”——成千上万文件逐个排查与旧版的不一致，且因为依赖类型论的复杂性，连最基础的证明都要在“裸机”状态下手工构造，宛如汇编级编程。业界一度认为 Sebastian 和嘉宾不可能完成，最终成功后嘉宾激动地打电话给对方。

第（十）部分 证明助手生态对比：Lean 的护城河与依赖类型论的优势（76% - 86%）

Lean 的极致可扩展性：因为 Lean 用 Lean 自己实现，用户可以在证明文件中间直接写宏/元程序来扩展 Lean——AI 现在甚至会自己给 Lean 写元程序来验证猜想。法国数学家 Patrick Massot 仅凭数学背景，就写出了名为 Labos 的扩展，把证明语言改成类似英语/法语教科书的自然语言风格，并做了点击式 Info View，全程未咨询核心团队。

mathlib 与社区：Lean 拥有庞大的数学库和活跃社区，过去用户在 Zulip 上提问常 5 分钟内得到人类答复；团队对用户（如首位重量级用户陶哲轩）的反馈响应极快，当天即可修复或加新特性，这是 Lean 社区飞轮的关键。

依赖类型论 vs. 高阶逻辑（HOL）：

• 嘉宾最初倾向选更易实现的 HOL，但陶哲轩等数学家明确指出：要吸引菲尔兹奖级别的数学家，必须用依赖类型论。
• 依赖类型的威力：类型的合法性可依赖于值。例如定义一个结构，其中某个字段的类型是“x > 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 预订链接。