我们是否被 Lean 卡住了？– 社区对 Lean 证明助理替代方案的观点
简短回答：Lean 的主导地位是一种社会技术锁定，而非技术必然性
Lean 是形式化现代数学的事实标准，因为它拥有庞大的库（Mathlib）、完善的工具链和机构支持。转向 Metamath、Isabelle 或 Coq 等替代方案需要相当的库、资金和社区动力，而这些目前都缺乏。
1. 为什么 Lean 今天看起来“不可避免”
- Mathlib 的规模 – Mathlib 包含约 250 万行形式化数学，由充满活力的社区持续扩展。仅凭规模就使 Lean 成为许多研究者最具生产力的环境。
- 全职开发 – Lean Formal Research Organization（FRO）为开发者提供资金，维护在线编辑器，并提供包管理器、语言服务器和文档工具。这种专业支持的水平在证明助理中罕见。
- 网络效应 – 大多数使用证明助理的数学家已经在 Lean 上共享他们的工作，使协作和代码复用变得直接。正如一位评论者所指出的，“我们使用的工具是一种社会学现象”。
- 近期的可靠性漏洞 – 虽然 Lean 曾出现一次高调的内核漏洞（嵌套归纳类型），但社区迅速修补，表明即使是大型项目也能从此类挫折中恢复。
“我们‘被 Lean 卡住’的程度，就像过去‘被 Internet Explorer 卡住’一样。” – Jacques Carette（MO 回答）
2. 存在的替代方案及其提供的功能
| 系统 | 基础 | 内核规模 | 显著优势 | 当前局限 |
|---|---|---|---|---|
| Metamath / Metamath Zero | 经典 ZFC（或其他公理体系） | ~700 行代码（Python 验证器） | 极小内核，绝对的证明透明性，多种独立验证器 | 自动化极少，手动证明工作量大，与 Mathlib 相比生态极小 |
| Isabelle/HOL | 高阶逻辑 | 较大（≈10 k 行代码） | 成熟的 IDE（jEdit），强大的自动化，历史悠久 | 用户界面显得陈旧，对依赖类型关注较少，纯数学库较小 |
| Coq | 归纳构造演算 | ≈10 k 行代码 | 强大的 tactic 语言，社区庞大，工业应用 | 纯数学库（Coq‑stdlib）远小于 Mathlib |
| Mizar | 集合论（Tarski‑Grothendieck） | 中等 | 形式化数学的悠久历史 | 现代工具有限，开发节奏较慢 |
| F* | 带副作用编程的依赖类型 | 中等 | 为程序验证而设计，集成 SMT 求解器 | 尚未在纯数学领域广泛采用 |
社区对替代方案的评论
- Metamath 的吸引力 – 其内核极小，证明完全显式，提供最高的正确性保证。一位贡献者强调了在 6.35 秒内验证 47 000 条定理的运行，凸显了检查的速度。
- 可用性担忧 – 多位受访者强调，证明助理不仅仅是内核；它还包括编辑器、自动补全、包管理和文档。Lean 的生态系统在这方面表现出色，而替代方案往往缺乏可比的前端。
- 基础偏见 – 有人认为基础（类型论 vs. 集合论）的选择应次于用户体验。正如一位回答所说，“基础并不是关键问题；大多数可用性来自设计良好的库和工具”。
3. 机构和财政因素
- 金钱重要 – 构建和维护现代证明助理需要全职开发者。Lean FRO 的预算支持持续改进，而大多数替代方案依赖志愿者努力。
- 潜在赞助者 – 如 INRIA 等组织已经资助 Coq；类似的支持可以让竞争者变得严肃。然而，没有主要机构宣布专门的计划来取代 Lean。
- 经济激励 – 一些评论者将此情形比作早期汽车制造商：先行者常常输给后来的、更好设计的产品。如果大型科技公司将形式化验证视为战略资产，他们可能会投资新助理，从而有可能打破 Lean 的垄断。
4. AI 的作用与未来互操作性
- AI 生成的代码 – 最近的 AI 项目已经生成了超过一百万行 Lean 代码，接近 Mathlib 的规模。这表明 AI 可以帮助为其他系统启动库。
- 跨系统翻译 – 借助强大的语言模型，系统之间（例如 Lean ↔ Metamath）自动翻译证明变得可行。lean‑to‑mm0 和 Dedukti 等项目已经在探索此方向。
- 验证流水线 – 将同一证明在多个助理中运行可以提供额外的信心，正如 Hacker News 的一条评论所示：“还有什么比在多个不同系统上同时运行来交叉检查证明更好的方法？”
5. 社会动态与社区锁定
- 高知名度数学家的影响 – Lean 的采用因 Kevin Buzzard、Peter Scholze 和 Terry Tao 等人物而加速。一条评论警告说，“特定技术在数学界的推广如此依赖于是否有某位特别著名的数学家在特定时间点使用该技术”。
- “vibe‑coding” 的担忧 – 一些社区成员担心 Lean 社区的文化可能更重视快速开发而非严格验证，可能导致对证明的“vibe‑coding”。
- 可移植性挑战 – 即使新助理的库规模匹配 Lean，迁移现有形式化也并非易事；许多需要重写，这是一大障碍。
6. 底线评估
- 技术可行性 – 从技术上讲，构建可行的替代方案是可能的（Metamath 的小内核、Isabelle 的成熟 IDE、Coq 的 tactic）。主要障碍是库规模和工具链。
- 机构支持 – 没有专门的资金和全职开发团队，替代方案在短期内不太可能达到 Lean 的成熟度。
- 社区动力 – 目前围绕 Mathlib 的网络效应使 Lean 成为大多数数学家今天最实用的选择。
- 未来展望 – AI 驱动的翻译和潜在的企业投资可能最终降低切换成本，但目前数学社区仍然实际上“被 Lean 卡住”。
本综合仅基于 MathOverflow 的提问、其七个回答以及 Hacker News 的热门评论，并在适当位置保留直接引用。