Why Lean? - Lean创造者亲述为何Lean是未来
Leonardo de Moura是Lean定理证明器的创造者，这篇文章是他亲自解释为什么Lean是未来。
核心洞见
Lean用Lean实现 — 所有编译器、elaborator、证明自动化、解析器、pretty printer、构建系统、文档系统都是Lean。没有 OCaml 和 Ltac 之间的粘合代码。
主要观点
1. 自举实现的力量
- 一个关键决策：一切都是Lean
- 因为聪明的人可以用Lean本身访问Lean的内部结构，他们构建了我们从未计划的东西
- Mathlib社区写了超过50,000行扩展（自定义tactics、linters、自动化），没有我们的协调
- Verso（文档系统）建立在Lean之上
2. 可扩展性
- Mathlib有超过200,000个定理和220万行代码
- 构建时间持续减少
- 愿意抛弃不工作的设计：已替换了类型类解析系统、simplifier基础设施、旧编译器等
3. 声音性（Soundness）无妥协
- Lean有一个小型trusted kernel
- 存在多个独立实现， proofs可以导出并交叉验证
- 构建了Comparator工具，跨kernel实现交叉检查proofs
- 关键洞察："建立疯狂metaprogram。写自定义tactics，以你几乎不理解的方式重写你的目标。kernel仍然会在最后检查一切。如果你的proof能通过类型检查，那就是正确的。"
4. AI安全的启示
Terence Tao的观点："RL会发现验证流程中的所有后门，所以不能有任何后门。强化学习太擅长发现这些后门了。"
这意味着：soundness不仅仅是理论属性，它是AI安全基础设施
5. 诚实的自我认知
- Lean的缺点：向后兼容性差
- 故意打破东西，因为可扩展性比接口稳定性更重要
- 如果需要2020年的代码在2026年还能编译，Lean不是那个系统
- 依赖类型理论是用户需要的，而不是最初想要的
为什么这重要
这是Lean创造者首次亲自解释Lean的核心设计哲学。在AI时代，形式化验证正在变得至关重要——因为RL会发现任何后门，所以系统必须从根本上sound。
Lean的设计理念：可扩展性 > 稳定性，小型trusted kernel > 大型复杂实现。