微软用15年造了个"数学外挂"，程序员看完集体沉默

2006年，微软研究院的一群人决定做件"蠢事"：用数学证明程序不会崩溃。当时没人觉得这事能成——毕竟写代码已经够累了，谁还想给代码写"数学作业"？

15年后，这个叫Lean的项目跑通了。不是跑在实验室里，是跑在数学家证明庞加莱猜想的现场，跑在本科生的期末作业里，现在还要跑进你的VS Code。

从"没人用"到"抢着用"：一个定理证明器的逆袭

Lean的诞生带着典型的学术气质。微软研究院的Leonardo de Moura想解决一个老问题：怎么让计算机帮忙验证数学证明是对的。这活儿以前叫"形式化验证"，属于那种听起来很酷、用起来很虐的工具——你得先把证明翻译成机器能懂的语言，比写证明本身还费劲。

Lean的前两代（Lean 1和2）基本没人记得。转折点在Lean 3，团队做了个关键决定：把定理证明器做成通用的函数式编程语言。数学家可以用它写证明，程序员可以用它写代码，两边互不耽误。

这个定位让它意外破圈。2020年，菲尔兹奖得主Timothy Gowers在博客写了一句：「Lean可能是未来数学家的标准工具。」同年，Kevin Buzzard带着帝国理工的学生，用Lean形式化了整个本科数学课程体系。

到Lean 4发布时，事情变得更有趣了。它不再只是"数学家的IDE"，而是一个能编译成C代码、性能接近原生、还带垃圾回收的通用语言。de Moura的原话是：「我们想造一个程序员真的想用的工具。」

函数式编程的"隐藏副本"：为什么选这条路

Lean的底层设计藏着个反直觉的选择：纯函数式（Pure Functional）。没有可变状态，没有副作用，所有计算都是数学意义上的函数——输入确定，输出就确定。

这听起来像自找麻烦。毕竟现实世界的程序要读写文件、要发网络请求、要改数据库状态。但Lean的答案是：把这些"脏活"用Monad（单子）包起来，和纯计算严格区分。

Monad这个从范畴论借来的概念，在Lean里成了安全边界。你的核心算法可以保持"数学纯净"，副作用被隔离在类型系统的监管之下。编译器会检查：你是不是在纯函数里偷偷干了不该干的事？

这种设计让Lean特别适合一类场景：你需要绝对确定代码没bug，而且愿意为此付出额外成本。比如加密算法、金融合约、医疗设备的控制逻辑——或者，数学家那个长达几百页、审稿人看了三年的证明。

2021年，Peter Scholze（另一个菲尔兹奖得主）在Nature发文，宣布他和Dustin Clausen的"液态张量实验"证明被Lean验证。这个证明的复杂度让传统审稿流程几乎不可能完成，Lean却把它拆成10万行形式化代码，逐行检查过了。

VS Code里的"证明即代码"：产品化路径

Lean 4的产品化做得相当克制。没有新建IDE，而是做了VS Code插件；没有造轮子，而是用LLVM做后端编译。de Moura的团队显然明白：工具再强，用户迁移成本太高也是白搭。

插件的体验很产品经理思维。你写证明的时候，编辑器实时显示当前目标（Goal）和可用策略（Tactics），像在玩一个解谜游戏。错误不是红字报错，而是"这里还缺一步"的引导式提示。

更隐蔽的设计是Mathlib——社区维护的数学库。这个库现在有超过100万行形式化代码，覆盖从线性代数到代数拓扑的标准内容。数学家写新证明时，可以直接引用库里的定理，像调用API一样。

这种"可组合性"是函数式编程的老优势，但Lean把它做成了学术基础设施。2023年，Terence Tao用Lean验证了一个关于多项式Freiman-Ruzsa猜想的证明，整个过程在GitHub公开，任何人可以复查每一步。

从学术玩具到工程工具的鸿沟

但Lean的野心不止于数学。团队正在推的"Lean for the working programmer"路线，试图解决一个更实际的问题：普通软件能不能也用形式化验证？

目前的答案是"能，但有条件"。Lean可以编译成高效的C代码，性能测试显示某些场景接近手写C。但形式化验证的成本依然很高——你需要先写规范（Specification），再写实现，最后写证明两者等价。三倍代码量起步。

de Moura的回应很直接：「不是每个函数都需要证明。但关键路径上的代码，比如密码学的核心实现，值得这个投入。」

这种分层思路正在落地。AWS的加密工具包部分模块用了形式化验证，Google的Chrome有类似尝试。Lean的优势在于，它让这种验证可以用同一套语言完成——写代码和写证明不需要切换上下文。

一个被反复提及的案例是seL4，一个经过形式化验证的操作系统内核。它的验证用了Isabelle/HOL，另一个定理证明器。但Lean社区有人在做类似尝试，而且试图把验证成本降下来。

15年后的现在，谁在为确定性买单

Lean的GitHub仓库现在有接近4000个Star，Mathlib的贡献者超过300人。这些数字在开源世界不算显眼，但用户的含金量很高——菲尔兹奖得主、顶尖高校的数学系、对安全极度敏感的工业团队。

微软对这个项目的投入也很有意思。研究院的项目通常有"孵化期"，但Lean持续了15年，而且明显在加大工程化力度。一个可能的解释是：云服务的安全需求在升级，形式化验证从"学术奢侈品"变成"工程可选项"的时机正在成熟。

de Moura最近在访谈里被问到：「Lean会取代传统编程吗？」他的回答很产品经理：「不会。但未来的关键系统，可能会默认包含形式化验证的模块，就像现在默认包含单元测试一样。」

这个预测能不能兑现，取决于一个更底层的问题：程序员愿不愿意为"数学确定性"支付额外的认知成本？Lean把门槛降了很多，但还没降到零。

你在写代码的时候，有没有遇到过那种"要是能证明这没bug就好了"的时刻？如果证明这个功能的成本，从"写一篇论文"降到"写三倍代码"，你会用吗？