最近刷 AI 证数学新闻的朋友，大概率都看过这条：8月1日，OpenAI 公布其下一代模型 Astra 的内部版本在数学和理论计算机科学领域取得十项重要进展，拿下 10 道十几年没人解开的难题，每道题都附了一份能被机器逐行检查的 Lean 证明证书。微博绿色对勾背后到底能保什么，我们前一篇已经聊过，今天不重复。
今天想聊的是另一条热度没那么高、但对程序员更要紧的消息：那批成果发布不到十天，播客 The Peterman Pod 请到了 Lean 和 Z3 的创造者 Leonardo de Moura，他现在是 AWS 的高级首席应用科学家，也是 Lean 背后非营利研究组织 Lean FRO 的联合创始人兼首席架构师。他在节目里说，自己已经不再写测试了，现在的工作方式是"我写性质，然后 AI 替我证明"。
形式化验证是不是真要告别"高贵但没用"？现在花时间学 Lean 值不值？这篇文章把成本账算给你看。
以前搞形式化验证，到底有多贵
先说个基准数据。形式化验证圈的标杆工程 seL4，一个被完整验证过的微内核，只有大约 8700 行 C 代码，验证总共花了约20人年的工作量，每行代码的验证成本约350美元。知乎AWS 用了十年形式化验证，也只敢用在最关键的安全组件上。de Moura 自己的总结是：如果写程序花 x 时间，过去做形式化验证就要花 10x。
而且注意，最痛的还不是初始投入，是维护。代码一直在变，每次改动都可能把已有证明弄坏——就像改了代码测试全红，只是修证明比修测试难得多，因为你可能早忘了当年那条证明背后的逻辑。这才是形式化验证几十年"不实用"的真正原因：不是理论不行，是人力成本算不过账。
AI 到底改变了什么
这次访谈里，de Moura 没怎么谈概念，给的都是实例。他的同事 Kim Morrison 干了一件他几个月前还认为不可能的事：用 AI 松散监督，把 C 语言压缩库 zlib 翻译成 Lean，并证明了对压缩引擎最要命的性质——压缩后再解压，一定恢复原始数据。整个过程大约一周，仓库里 1100 多条定理、约 32000 行证明代码，没有一个未完成的占位符。对比 seL4 的"8700 行、20 人年"，成本单位从"人年"变成了"周"。
Lean 的证明写出来就是一段代码。社区里流传的一个直观例子，是有人把 2026 年高考数学全国卷 I 的压轴题完整形式化，满屏都是 tactic 推导链。知乎
de Moura 自己现在也直接对 AI 下指令："请在不使用某个特性的情况下重写这些证明。“哪怕那些证明不是他写的、他甚至不知道是关于什么的，AI 也能很快交出新版本。他对此的总结很直白——过去他的超能力是"能忍受很多痛苦”，现在这个超能力不值钱了。知乎
还有一个反常识的点：很多人以为形式化验证难在"写规格说明"。de Moura 说不一定。你可以用最朴素、最慢、最容易理解的版本当规格，让 AI 生成高效版本，再证明两者等价——"和朴素版本等价"就是所有优化的关卡。有了证明，优化就是免费的。
机器验证的结果，凭什么信
Lean 的可信度不来自"Lean 这个软件完美无缺"，而来自你只需要信任它的内核——只有大约5000行代码，小到任何人都能自己从头写一个，证明检查本质上就是类型检查。知乎社区已经有多个独立实现的 Lean 内核互相印证，有人用 Lean 本身写了 Lean4Lean 内核并证明了其正确性，还有 Rust 实现。多内核交叉验证，是目前最硬的保障。
但也要记住前一篇的结论：机器验证保的是"证明和所证命题一致"，不保"所证命题就是你想要的那个"。举个更接地气的例子：此前有人宣称用 Lean4 验证了 P=NP，动静不小，结果社区扒开仓库一看，主定理证明的其实是 True=True 这种恒真命题——机器照样亮绿灯，但证的和 P=NP 没什么关系。知乎Astra 的十项成果里也一样，最受关注的 Connes 刚性猜想反例，已有反驳文章声称 OpenAI 构造的群不满足原猜想的前提条件。微博绿色对勾是下限，不是上限。
所以现在值得学吗，看你是哪类人
我的判断分三档。
现在就可以上手的，第一类是做系统、安全、Rust、函数式方向的工程师。验证成本已经从"只配关键组件"跌到"日常项目可以试"，Aeneas 这类工具链已经能把 Rust 代码映射成 Lean 来验证，这条线只会越来越实。
第二类是数学专业或有竞赛背景、想往 AI 定理证明方向走的人。官方有 8 个游戏化教程可以入门。知乎陶哲轩第一次用完 Lean 说"我大概不会再用了"，一周后开了第二个项目——学习曲线真实存在，但回报曲线也变陡了。这类人还有个绕不开的背景：2024 年 DeepMind 的 AlphaProof 用 Lean 拿到国际数学奥林匹克银牌，到 2025 年，Harmonic 的 Aristotle 系统和字节跳动的 Seed-Prover 都已用 Lean 形式化证明达到金牌水平。知乎de Moura 的原话是，现在大家把它当简单问题的基准。
第三类是想做 AI 证明 Agent 的人。Lean 就是现在事实上的训练场和验收场，想入这个门，绕不开它。
可以再观望的：日常写业务接口的朋友不必焦虑。形式化验证的主战场仍在系统底层和数学基础设施，它不会直接影响你明天写 CRUD。把它当兴趣关注即可，盯三个信号：Lean FRO 公布的项目方向、社区挑战平台上"要求构造数学对象"的题目（那是目前 AI 的能力边界，de Moura 自己承认 AI 还没展现出提出新数学概念的能力）、以及 Rust 验证工具链的成熟度。
真想学，路线和坑都在这里
最大的坑不是数学，是环境：工具链用 elan 装，mathlib 大库用 lake 拉，缓存文件动辄几千个。有人实测 Astra 的证明仓库，全量编译 lake build All 跑了 34 分钟才把十个模块全部验证完。哔哩哔哩机器性能弱的，第一步就卡住。所以建议分三步走。
第一步，先别装环境。浏览器直接打开自然数游戏（Natural Number Game）网页版，花两个小时感受"证明是什么"。这个游戏免费、零安装，通关率就是最诚实的兴趣测试。
第二步，想系统学，看今年 6 月上线的《逻辑验证漫游指南》2026 中文版，由 Lean-zh 项目组翻译。知乎此前中文资料稀缺一直是最大门槛之一，这个门槛刚刚被拆掉。
第三步，再碰 Mathematics in Lean 和 mathlib，尽早对真实对象动手。已经有人用 Lean4 去完成《算法导论》的大部分课本证明，甚至有人手搓高考压轴题，以战代练是最快的。知乎
最后说一句：这条新闻不是"数学已死"，而是证明正在从顶级数学家和关键基础设施的专属品，变成工程师的日常工具。de Moura 说形式化验证的痛苦正在消失，更准确地说，是痛苦被 AI 接走了，留给人的部分反而更值钱——决定哪些性质值得被证明。
