近年来，形式化数学在学术社区引发了一波复兴浪潮。Lean 作为目前最活跃的交互式定理证明器之一，凭借其强大的类型论基础和丰富的数学库 mathlib，正吸引越来越多的工程师和数学爱好者投入学习。对于具备常规编程背景但缺乏形式化验证经验的开发者而言，入门 Lean 面临着双重挑战：既要掌握依赖类型论的核心概念，又要适应函数式编程的思维方式。本文将从工程化视角出发，系统梳理从零基础到能够独立完成基础形式化证明的学习路径，并给出可量化的阶段目标与实用工具推荐。
理解 Lean 的定位是首要问题。Lean 既是一门基于依赖类型论的函数式编程语言，也是一个交互式定理证明器，这一双重身份决定了它的学习曲线比普通编程语言更为陡峭。与传统命令式语言不同，Lean 中的证明与程序共享同一套语法结构，这便是 Curry-Howard 同构定理在实践中的体现：程序即证明，证明即程序。然而在实际使用中，证明与计算仍然被划分为两个不同的宇宙 ——Prop 与 Type，两者在语义和工具链上存在微妙差异。理解这一点对于避免初期的概念混淆至关重要，很多新手正是由于未能区分这两个层面而在 tactic 编写时频繁受挫。
依赖类型论是 Lean 最核心也是最难以直观理解的概念。与传统类型系统不同，Lean 采用了三层对象层级结构：terms（项）位于底层，types（类型）位于中层，而 universes（宇宙）位于顶层。每一个 type 本身都归属于某个 universe，而 universe 又有其上一层的 universe，形成递进的层级关系。举一个具体例子，在 Lean 中可以看到 3 : Nat、Nat : Type、Type : Type 1 这样的层级表达。这种设计使得类型本身可以作为值来处理，从而支持诸如 Fin n（长度为 n 的有限类型）这样依赖于值构建的复杂类型。对于工程师背景的学习者而言，初期最大的认知障碍在于：类型不再仅仅是静态的标签，而是可以参与计算的一等公民。这种 “类型即数据” 的思维转变需要刻意练习才能逐步适应。
关于学习资源的选取，社区已形成相对成熟的梯度路线。对于完全的零基础，推荐从 Natural Number Game 和 Set Game 这两个在线交互式教程入手。它们以游戏化的方式引导学习者完成自然数和集合论基础的形式化证明，让你在解决谜题的过程中自然习得 Lean 的基本语法和证明策略，而不必一开始就面对铺天盖地的类型论术语。这一阶段的投入时间建议控制在两周以内，以每天一到两小时计算，重点在于建立直觉而非追求深度。接下来可以转向 Mathematics in Lean，这本教材与传统的数学教材风格接近，以具体数学内容为载体逐步引入 Lean 语言特性，学习节奏更为自然，适合已经具备本科数学基础的学习者。同时，Theorem Proving in Lean 4 则更适合作为补充参考，它从编程语言理论的视角系统讲解 Lean 的语言机制，适合在具备一定实践经验后回过头来阅读，以填补概念层面的空白。
在实际学习过程中，常见的入门陷阱值得提前规避。第一个高频错误是忽略类型类的隐式机制。Lean 中的数值字面量实际上是类型类多态的，比如直接写 1 可能被推导为整数、有理数或实数等多种类型，初学者经常会因此收到令人困惑的类型错误。解决方法是明确标注类型，例如 (2 : ℕ) 可以消除歧义。第二个常见问题是遗漏 by 关键字 —— 在 tactic 模式中编写证明时必须使用 by 来引入 tactic 块，否则 Lean 会将后续内容当作常规函数定义来解析。第三个易错点是使用 | 代替 \| 来表示整除关系，在 Lean 中 | 是管道操作符，而整除关系需要转义。这些细节虽然看似琐碎，却是导致新手放弃的主要因素，建议在入门阶段将这些模式总结为个人速查卡片以供参考。
进入中等阶段后，需要逐步掌握核心 tactic 的组合使用。基础 tactic 包括 intro（引入假设）、cases（分类讨论）和 induction（数学归纳法），这三者构成了大多数证明的骨架。当你能够熟练运用这些基础工具后，应当进一步学习超级 tactic—— 即能够自动完成复杂化简或计算的高级工具。simp 是最常用的化简 tactic，它根据预定义的规则库自动改写目标表达式；ring 专门处理环结构的代数运算；linarith 处理线性算术不等式；而 aesop 则是一个更通用的自动化证明搜索工具。这些超级 tactic 大幅提升了证明效率，但它们的行为模式和性能特征各有不同，需要通过大量实践来积累直觉。值得注意的是，自动化 tactic 并非万能 —— 它们在处理需要创造性构造的证明时往往力不从心，此时仍需依赖手工编写的策略性证明步骤。
工具链的完善对于高效学习同样不可或缺。VS Code 配合 lean4 扩展是最主流的开发环境，提供了语法高亮、目标状态实时显示、定义跳转等核心功能。当在证明过程中遇到卡顿，可以使用 Loogle（Lean 的类型搜索引擎）查找库中已有的类似定理，类似于面向类型签名的 Google 搜索。此外，Lean Zulip 社区是解决疑难问题的最佳去处，社区成员活跃且对新手的提问非常友好。另一个值得掌握的技巧是利用 IDE 中的 LLM 自动补全功能（如 GitHub Copilot），它能够根据上下文提示可能的证明策略，虽然不完全可靠，但作为思路启发工具效果显著。根据实际经验，建议将每日学习目标量化为 “完成三道中等难度练习题”，通过持续的小规模反馈保持学习动力。
形式化验证的长期价值不仅在于提升证明的严谨性，更在于它改变了思考问题的方式。通过将数学证明转化为可执行的代码，你会在形式化过程中自动暴露那些在直觉层面容易被忽略的假设和逻辑漏洞。这种能力在软件工程领域尤为宝贵 —— 形式化方法的思维可以帮助你设计更健壮的 API、编写更可靠的测试用例，甚至在代码审查中识别潜在的边界条件错误。正如 Knuth 所言，编程是一种艺术，而形式化验证则是将这种艺术推向精确极限的手段。
参考资料
- Rado Kirov, Learning Lean 系列博客: https://rkirov.github.io/