从测试到证明：Lean创始人谈AI如何让形式化验证成本降低10倍

主持人以Dijkstra的名言开场：“程序测试可用于揭示bug的存在，但永远无法证明bug的不存在。”这句话道出了传统软件验证的边界。而Lean这类形式化验证工具，恰恰要跨越这条边界——不是“发现”bug，而是从逻辑上“证明”bug不可能发生。这正是形式化验证的根本价值所在。

Lean既是一门编程语言，也是一个证明系统。作为编程语言，它可以写代码；作为证明系统，它可以对代码写出性质，并用机器可检查的证明来验证这些性质。它提供的是绝对正确的保证，并且拥有多个独立的检查器，确保证明结果可信。更准确地说，Lean应被视为一个平台：你可以在这个平台上写代码、写关于代码性质的命题、并给出机器可验证的证明。本期节目围绕它如何工作，以及它如何改变数学与软件验证的未来展开，并提出了一个核心疑问：手写数学是否会终结？

首先，Lean到底是什么？它本质上是基于依赖类型论（Dependent Type Theory）的一族证明助手（如Rocq/Coq和Lean）中的一员。这类工具天然就是“编程语言+证明助手”的一体两面。在软件验证领域，目前存在两种主流路径：其一是浅嵌入（Shallow Embedding），通过工具（比如把Rust翻译到Lean的转换器）将其他语言映射到Lean中进行验证；其二是深嵌入（Semantic Modeling），在Lean中为C语言等编写形式化语义，把C程序表示为Lean中的数据结构，从而对其陈述性质并进行推理。举例来说，若要验证一个C语言访问数组的操作不会越界，可以在Lean中把“索引i满足0 ≤ i < 10”写成数学命题，而原来的C源文件则对应一份“元数据式”的Lean证明，由Lean逐行检查该命题是否成立。整个过程的自动化程度取决于所建立的框架，比如基于前置条件-语句-后置条件的三元组结构。复杂度是软件验证的大敌，而AI的出现让“自动证明”成为可能，但前提是证明必须写成模块化的形式，以便扩展。

接下来看测试与形式化证明的本质差异。测试套件再全面，也只覆盖了有限场景，角落案例仍可能遗漏；而形式化证明覆盖所有可能情况，真正做到了“bug的不存在”。一个震撼案例是：主持人的同事Kim Morrison发起了一个项目，让AI把C语言编写的Zlib压缩库翻译进Lean，要求它通过原测试套件，并证明一个强性质：“压缩后再解压得到原始数据”。结果，仅用一周时间就完成了整个形式化工作。目前剩下的任务只是性能优化，且优化时不能破坏已有的证明。

但是，写出一份好的规格（Specification）本身就是一种成本，且随程序而异。一个实用技巧是：先用“低效但正确”的实现作为规格，再让AI生成高效版本，并证明高效版本与这个规格等价。这样不仅降低了书写规格的难度，还能利用AI自动生成证明。工业界已有先行者：Jane Street等公司正在投资形式化验证，例如对微内核seL4的完整验证。过去在没有AI的情况下，“手动证明+维护证明”的成本极高——经验上往往达到编写程序本身工作量的10倍。而AI正在消除这种痛苦，因为它非常擅长撰写和维护形式化证明，即使人类已经忘了当初为何这样证明。

Lean不仅是一个证明助手，更是一门生产级编程语言。AWS内部就有一个约50万行Lean编写的AI加速器编译器，主要把Lean当编程语言使用，顺带获得一些性质证明作为“额外红利”。其工具链体验也已接近现代语言：构建系统Lake相当于Rust的Cargo，编辑器使用VS Code，提供IntelliSense等熟悉功能。最特别的是Info View这一核心交互界面——屏幕通常一分为二，左侧是代码/证明文件，右侧实时显示当前证明目标的状态变化，给用户持续反馈。Tactic模式则将证明过程变成“游戏”：用户通过`by`进入领域特定语言DSL来写证明，每一步可以简化目标、应用已知引理等，看着目标逐步减少直到归零，过程极具“通关”快感，不少用户戏称自己“沉迷其中”。

最后，关于内核信任问题。Lean整体是一个庞大的系统，且规格频繁变动（例如简化器的行为不断被用户定制），难以对全部代码进行形式化验证。但Lean的设计哲学是：只需信任极小的内核。底层类型检查器是整个系统的信任根，其他部分（如宏、化简器等）可以替换或绕过。同时，Lean拥有多个独立的检查器，即使内核存在bug，其他实现也可能将其暴露。这种“最小化信任面”的做法，使得形式化验证的结果依然具有极高的可信度。

总而言之，Lean结合AI，正在把形式化验证从“高不可攀”变成“触手可及”。它不仅能证明数学定理，还能验证软件正确性，并且有望将验证成本降低一个数量级。手写数学是否会终结？答案或许就藏在Lean的证明搜索中。