上周，一篇访谈整理在形式化圈子里传开了。Lean 和 Z3 的创造者 Leonardo de Moura 在播客里说：“我已经不再写测试了。我写性质，然后 AI 替我证明。”知乎
比这句话更扎眼的是他给的两个数字。一个是旧世界的标杆：完全形式化验证的微内核 seL4，只有大约 8700 行 C 代码，验证花了约 20 人年，算下来每行代码的验证成本约 350 美元。另一个是新世界的样本：他的同事 Kim Morrison 用 AI 把 C 语言压缩库 zlib 翻译成 Lean 并完成全部验证——包括证明"压缩后再解压一定能恢复原始数据"——整个过程大约一周，仓库里 1100 多条定理、约 32000 行证明代码，没有一个留坑的占位符。知乎
从 20 人年到一周，这不是效率提升，是成本结构变了。
先看看这一年到底发生了什么
伏笔其实埋了两年。2024 年，DeepMind 的 AlphaProof 用 Lean 拿下国际数学奥林匹克（IMO）银牌；2025 年，Harmonic 的 Aristotle 和字节的 Seed-Prover 都做到金牌水平。知乎de Moura 说自己几年前认为 IMO 金牌不可能，“现在大家把它当成简单问题的基准”。
到了今年，节奏明显加快。5 月，OpenAI 宣布其模型反驳了 Erdős 的单位距离猜想，Lean 社区随即发布形式化挑战，OpenAI 的 Boris Alexeev 用大约两周完成完整形式化，含依赖库约 100 万行代码。知乎8 月 1 日，OpenAI 的 Astra 模型又拿出 10 个横跨 8 个领域的开放问题，每个都带 Lean 4 证明证书。哔哩哔哩
数学界的态度也在转弯。菲尔兹奖得主 Scholze 曾把自己都不确定对错的重要结果交给 Lean 社区验证；陶哲轩第一次用完说"我大概不会再用了"，一周后开了第二个项目。知乎今年 3 月他发布 26 分钟实操视频，演示用 Claude Code 在 Lean 里做证明，中途两度因为 token 不够用宕机。麻省理工科技评论去年 9 月，一个叫 Gauss 的 AI 用三周在 Lean 中形式化了强素数定理，而陶哲轩手工推进 18 个月才到一半。量子位
AI 真正打掉的是维护成本，不是证明成本
很多人的第一反应是：AI 变得这么会证题了？de Moura 的回答更有意思：写证明从来不是最痛苦的部分，维护才是。
可以把形式化验证理解成一套极端严格的测试：程序每改一次，对应的证明就得跟着修。代码天天在变，证明天天在断，而且修证明比修测试难——你可能早忘了当初为什么这么证。过去形式化验证的总成本大约是开发成本的 10 倍，大头就堆在这个环节。知乎而"按新约束重写证明"恰恰是 AI 的舒适区：de Moura 说自己让 AI 重写一段从没读过、不知道在证什么的证明，只要求避开某个特性，“AI 瞬间给出了新版本”。他对此的总结很直白：我以前以为自己的超能力是能忍受痛苦，现在这个超能力没用了。
顺带被改变的还有规格说明的成本。他的思路是：一个低效的程序本身就可以当规格说明——先用最朴素、最慢、最容易理解的方式写出"我要什么"，再让 AI 生成高效版本，并证明两者等价。知乎有了这道等价性关卡，AI 可以放心大胆地优化，因为任何优化都必须过证明这一关。
先泼一盆冷水：Lean 亮绿灯，不等于你证的定理是对的
这周社区恰好演示了一遍坑在哪。
7 月底，知乎出现一个提问："我们在 Lean4 重建了一座数学大厦并形式化了广义黎曼假设，请问大家能否找出逻辑漏洞？“高赞回答直接开拆：24 个未解决目标、一堆语法错误、不用官方维护的 mathlib 而是自定义公理系统，证明里还混着两套没对齐的"相等”。知乎这样的"证明"乍看气势恢宏，实际证的根本不是你以为的那个黎曼假设。8 月初"AI 证伪百年猜想被打假"的讨论里，被翻出来的也是同一个问题。
这就是形式化验证最要命的坑：Lean 只检查逻辑推演是否自洽，不检查你写的命题是否对应你真正想证的那个定理。定理证对了，题目抄错了，Lean 照样绿灯放行。微博
怀疑的声音也一直存在。8 月中旬还有研究者在小红书写"AI+Lean 在数学上的作用目前被严重夸大"——现阶段训练和评测数据仍要靠人类数学家出题、写答案、审题。小红书de Moura 自己也划了边界：AI 能找到已有问题的新证明路径、能反驳猜想，但到目前为止，没有证据表明它能提出新的数学概念。知乎门槛在降，判断力的门槛没降。
那么谁该入坑，谁该再等等
第一类：想走 AI4Math、形式化数学方向的学生——现在入场，时机比以往任何时候都好。 AI 接管了体力活，中文资源也补齐了：Lean-zh 中文社区已译介《Lean4 定理证明》《Lean4 形式化数学》《Lean4 函数式编程》《Lean4 元编程》四本官方教程。知乎路线是现成的：先玩 Natural Number Game（Lean 的网页闯关游戏，不少人反馈上手就上头），再跟《定理证明》打基础，然后进《形式化数学》和 mathlib。
B 站有"数理基要主义"等手把手更新的中文系列，浙大等高校暑期学校也在开课。哔哩哔哩国内团队同样在出活：北大 AI4Math 团队今年 4 月用自动化框架解决了交换代数开放问题安德森猜想，并完成 Lean 形式化验证。微博
第二类：对软件验证感兴趣的工程师——值得试水，先别上生产。 lean-zip 这个范式（AI 翻译 + AI 验证 + 证明守门下的优化）值得认真跟踪，Aeneas 这类工具已经能把 Rust 代码映射到 Lean，Mistral 也在 7 月开源了专门做 Lean4 证明的模型 Leanstral 1.5。微博招聘端开始有动静：蚂蚁技术研究院的 2027 届校招里出现了"AI+Math-Lean 语言形式化验证"岗位，方向写着 Rust 程序验证、密码学协议验证。微博但对存量生产代码来说，写规格和迁移生态的成本仍然高，适合先在高安全、小规模场景验证手感。
第三类：纯围观的普通程序员——不用急着装环境，把谈资收好。 今年干活还用不上它，但这组数字值得记住：IMO 从银牌到金牌、验证成本从 20 人年到一周、百万行形式化两周完成。想低成本参与，可以花一个下午玩玩 Natural Number Game，体验一下"用类型把算术证出来"是什么感觉。
最后留三个值得持续盯的信号：一是会不会出现更多像 lean-zip 这样的生产级验证案例；二是跨证明器翻译的进展——7 月底发布的 ITPEval 基准显示，LLM 在 Lean4、Rocq、Isabelle、HOL Light 四大证明器之间翻译定理语句，成功率最高只有 29.1%，空间巨大。哔哩哔哩三是 Lean 社区挑战平台上"要求 AI 自己构造数学对象"的题目被推到哪一步。这三条线动得比大众认知快。
