2026-09-30
微软与 KIT 把 Lean 用 Lean 重写并编译到 C。卫生宏、表式类型类、引用计数就地更新,用来拆掉 Lean 3 改不了核心、tactic 还吃解释器的两堵墙。
Lean 3 能做起来,靠的是可扩展和元编程。2017 年起社区用它堆 mathlib,写这篇时大约 50 万行,里面有概形 Scheme、perfectoid space,还撑起了 Peter Scholze 的 Liquid Tensor 挑战。库里不只是数学对象:有环论求解器、Presburger 算术判定、语义 linter;Galois 还拿 Lean 3 元编程做过 SQL 查询等价检查。
墙有两堵。解析器、elaborator、代码生成写在 C++ 里,用户改不了,除非去改系统源码。证明自动化如果用 Lean 3 元编程来写,要过虚拟机解释,跑不过同类 C++ 或 OCaml 实现。
Lean 4 的回答是把整套证明器用 Lean 重写,同时做成能出高效代码的函数式语言。2021 年初开源。
四个选择撑起这套自举。
卫生宏。Lean 3 的语法扩展是受限的「语法糖」替换,tactic 语言还有名字误捕获。Lean 4 从 Scheme 家族借来捕获回避,按交互式定理证明器的需求重做。对外是一层塔:infix 展开成 notation,notation 展开成 macro,macro 再拆成 syntax 声明加 macrorules。用户能停在够用的那一层,也能下到过程式宏。解析和展开分开,展开前就能拿到具体语法树,补全、跳转、重构才有结构可依。文中用布尔表达式 DSL 演示:[BExpr| p ∨ true] 会展开成构造子应用。
表式类型类解析。类型类在 mathlib 里用得很深,Lean 3 露出两项病:缺项索引带来多余开销,钻石继承会指数爆炸。新过程把 instance 看成 λ-Prolog 的 Horn 子句,用 discrimination tree 做索引,再用 tabling(逻辑编程里的记忆化)卡住重复目标。对应代码在 SynthInstance 和 DiscrTree。
代码生成。编译器走一串接近 GHC 的变换,但 Lean 是严格求值。@[inline] 和 @[specialize] 用来拆掉抽象塔。擦掉证明项后进入 IR,默认后端出 C;IR 本身是 Lean 数据结构,换后端可以只写 Lean。另有 IR 解释器,编辑器里能立刻跑;调用到已有 AOT 本地代码时切过去,解释开销可以压到可忽略。
内存管理用引用计数。观察叫 resurrection hypothesis:函数式更新里,旧对象常常刚好在同构新对象诞生前死掉。引用计数为 1 时就地改,不分配。这套写法叫 functional but in-place,简称 FBIP。map f as 在 as 不共享时零分配;as 是不共享的整数列表的列表时,map (map inc) as 同样零分配。和静态线性类型不同,只共享前缀时,未共享的尾巴照样就地更新。数组和哈希表因此能进纯代码,决策过程和证明自动化最吃这一项。
tactic 和 elaborator 也全部用 Lean 写。simp 是 mathlib 里最常用的 tactic 之一,用户能改它的实现。LSP 服务器用标准库的 task 抽象做增量分析,社区首选 VS Code。
这是一篇系统描述。正文没有 Lean 4 对 Lean 3、Coq 或 Isabelle 的证明性能对照表。能钉死的事实如下。
| 项 | 数字或事实 | 对照 |
| 项目起点 | 2013,基于 Calculus of Inductive Constructions | Lean 1/2/3 同一条线 |
| Lean 4 发布 | 2021 年初,开源 | 用 Lean 重写 |
| 当时 mathlib | 约 50 万行 | 仍是 Lean 3,正在移植 |
| 不共享 list 上的 map | 零分配 | 常规函数式要新分配 |
| FBIP 相对 ocamlopt / GHC | 论文称常常更快 | 数字在 Perceus 与 Counting immutable beans,本文没表 |
早期应用写了三个:Galois 的 Reopt 翻译验证器、归纳-归纳类型支持包、平衡车控制器。mathlib 移植完成度这篇没给。
写 tactic 的人终于有一条能落地的路径:自动化不再困在解释器里,可以编译成 C 再加载。想改解析器、elaborator、pretty printer、代码生成,也不必再提 C++ PR。
FBIP 是这篇对「纯函数式能不能快」最具体的答案。决策过程爱用哈希表,线性类型要你在类型里证明不共享;引用计数把检查推到运行时,不共享就地改,共享就复制。代价是运行时记账。
卫生宏把 ITP 的语法扩展从「再加一条 ad hoc 糖」收成一套可组合的塔。后面大量 notation 和嵌入式 DSL,都走这条路。这篇是设计说明书,不是评测报告。
作者写明这是长期项目。当时计划里有对接外部 SMT 和一阶证明器、新编译后端、把 Lean 3 的 mathlib 和 widget 库搬过来。这些在 2021 年初都还没做完。
本文几乎没有系统级评测。类型类「解决了钻石指数爆炸」的细节在 Selsam、Ullrich、de Moura 的 Tabled typeclass resolution;FBIP 的速度数字在 Perceus 技术报告和 IFL 2019 的 Counting immutable beans。读这篇无法独立核对「常常更快」有多快、在哪些程序上更快。
信任基仍是相对小的 kernel,宏、elaborator、tactic 的扩展面却拉得很开。扩展写错不会直接污染 kernel,但会污染用户看到的证明状态。论文没有讨论扩展作者怎样避免把错的 elaboration 当成证明。
Resurrection hypothesis 是经验观察,不是证明。数据结构经常共享时,FBIP 退回普通分配,就地更新帮不上。