这篇文章表达了作者对当前Lean语言在数学形式化领域占据主导地位的反思。作者回顾了数学形式化的历史，指出早在1968年AUTOMATH就实现了数学形式化，强调这一领域的发展并非始于Lean。作者赞赏Lean的优点，但也批评其社区存在的排他性和从众心理，提醒人们不要忘记前人的贡献。

标题：为何不直接使用Lean？

来源：https://lawrencecpaulson.github.io/2026/04/23/WhynotLean.html
发布时间：2026年4月26日

背景与争议

作者指出，如今在提议形式化数学时，常被要求解释为何不使用Lean。这让他联想到40年前离开依赖类型领域的原因：其封闭性、教条主义和从众心态。尽管Lean拥有优秀的工具、庞大的库和活跃的社区，但数学形式化的历史可追溯至60年前，其发展并非仅靠追随潮流。

历史回顾

1. AUTOMATH的开创性

   • 1968年，de Bruijn的AUTOMATH已具备数学形式化的核心要素。1977年，Jutting用它形式化了Landau的《分析基础》，包括从纯逻辑构建复数，并证明了实数线的戴德金完备性。
   • AUTOMATH的缺陷在于糟糕的符号系统和缺乏自动化，但其处理等价类的能力至今仍优于某些现代工具（如Rocq）。

2. Boyer-Moore的贡献

   • 1973年，Boyer和Moore提出以计算逻辑验证代码，虽在通用数学上有限制，但仍成功形式化了哥德尔不完备定理、二次互反律等深奥结果。其现代版本ACL2主要用于硬件验证。

3. LCF及其衍生系统

   • 爱丁堡LCF以函数式编程语言作为元语言（ML），影响了HOL、Coq和Isabelle等工具的发展。
   • HOL Light的John Harrison通过形式化实数分析证明了素数定理等成果，而Isabelle则通过“借鉴”HOL Light的成果实现超越。

Lean的崛起与局限

• 社区推动：Tom Hales和Kevin Buzzard推广Lean，构建高级数学定义库（如格罗滕迪克概形），使其在数学教学中流行。
• 放弃构造性证明：Lean社区摒弃了Rocq对构造性证明的执着，更贴近传统数学需求。
• 命题即类型的误区：作者批评将“命题即类型”视为唯一范式的观点，指出AUTOMATH和LCF均未采用此设计，且动态验证（如ML的抽象数据类型）足以确保证明正确性，无需庞大的证明对象。

为何选择Isabelle？

• 自动化优势：Isabelle的自动化工具（如sledgehammer）无与伦比。
• 可读性：结构化证明语言Isar（受Mizar启发）更易阅读。
• 避免依赖类型：依赖类型可能导致类型检查不可判定，而Isabelle通过灵活设计（如不强制所有对象为类型）支持复杂数学（如域扩张、p进数）。

未来展望

• AI与形式化：AI生成的证明虽杂乱，但可通过自动化工具优化，且结构化证明易于跨系统移植。
• 遗漏的Mizar：作者承认未提及Mizar及其庞大数学库的贡献，承诺后续补述。

结语：Lean虽优秀，但Isabelle在自动化、可读性和设计哲学上提供了独特优势。形式化数学的未来需兼顾技术多样性与人类可理解性。

（注：感谢Wenda Li的评论！）

以下是评论内容的总结：

1. 支持探索替代方案的观点

   • MarkusQ认为应该考虑不同的选择，即使最终选择主流方案，了解其他选项也有益处。
     • "For every 'well of course, just...X, that's what everybody does' group-think argument there's a cogent case to be made for at least considering the alternatives."
   • zermelo44简单表示赞同："Good post! +1"

2. Lean语言的实用性和编程视角

   • kccqzy提到Lean对程序员的价值，推荐了一本从函数式编程角度介绍Lean的书。
     • "it’s more relevant to consider the programming side of things... covers Lean from a functional programming perspective"
   • smj-edison指出Lean作为语言与Mathlib库的区别，强调其古典逻辑的实用性。
     • "Lean is a language, and what most people are talking about is a library called Mathlib... creators are very pragmatic"

3. Lean与数学和计算机兴趣的关系

   • groundzeros2015认为类型理论和Lean更吸引计算机爱好者而非数学爱好者。
     • "Type theory and lean is more interesting to people who like computers than to people who like math."
   • jsmorph分享了一个结合Go和Lean的实际项目案例，展示Lean在非数学密集型应用中的潜力。
     • "uses a Go/Lean hybrid design... Really just functional programming with some interesting proofs"

4. Lean与其他工具的比较

   • c0balt比较了Isabelle/HOL和Lean，指出两者各有优劣，但Lean在特定领域更高效。
     • "both languages mostly just made different tradeoffs... Lean just specialized for a different part of this space"
     • 批评Isabelle的工具和开发者沟通问题："Things like 'we don't have bugs just unexpected behaviour'... seems childish/unprofessional"

5. 对进一步讨论的期待

   • shaguoer表示对讨论感兴趣："Interesting perspective. Would love to see more discussion."

总结：评论主要围绕Lean语言的价值、应用场景和与其他工具的比较展开，既有对其实用性和编程视角的肯定，也有对其与数学和计算机兴趣关系的讨论，同时包含了对其他工具的比较和批评。