Lean 是一种开源软件，兼具证明助手和编程语言的功能，用于表达数学定义、构造证明，并验证证明是否符合精确的逻辑规则。它支持数学的形式化以及软件的形式验证。其架构的关键特点是，将辅助构造证明的复杂工具与检查最终证明项的较小内核分离。Lean 4 还可作为通用函数式编程语言，让用户在同一环境中编写程序并实现证明自动化。(lean-lang.org)
起源与发展
莱昂纳多·德·莫拉（Leonardo de Moura）于 2013 年在微软研究院启动了 Lean 项目。Lean 0.1 于 2014 年 6 月 16 日正式发布。该项目旨在将小型、可独立实现的证明检查器所提供的可靠性保障，与自动推理工具的便利性结合起来。这种结合使系统能够提供高度自动化，而不必将每一种证明构造过程都纳入受信任的逻辑核心。(lean-lang.org)
Lean 4 是一次大规模的重新实现，而不只是对早期版本的渐进式扩展。德·莫拉与塞巴斯蒂安·乌尔里希（Sebastian Ullrich）于 2021 年发表的系统介绍论文，描述了其可扩展的前端，以及主要使用 Lean 自身编写的实现。其功能包括用户自定义语法、宏、精化过程和证明策略。此后，数学社区借助名为 mathport 的移植工具，将数学库从 Lean 3 迁移到了 Lean 4；这两代系统的源代码并不兼容。(lean-lang.org)
逻辑基础
Lean 的基础是依赖类型论，其中类型可以依赖于值。因此，除了普通的函数类型和数据类型，还可以表达诸如按长度索引的向量类型。其核心理论包含依赖函数、归纳类型、类型宇宙的层级，以及专门用于命题的类型 Prop。类型宇宙将类型组织成不同层级，而不是将所有类型都视为某个不受限制的“全体类型的类型”的元素。(lean-lang.org)
命题与证明之间的关系遵循柯里—霍华德对应：命题表示为类型，而证明则是该类型的一个项。例如，蕴含命题 P → Q 的证明是一个函数，它将 P 的证明转换为 Q 的证明。因此，检查形式证明，就相当于检查其证明项是否具有所声称的定理对应的类型。(lean-lang.org)
归纳定义通过构造子及相应的消去原则来描述自然数、列表等对象。这些机制支持以递归方式给出定义，以及通过数学归纳法进行证明。Lean 还通过额外的原则支持经典逻辑推理，包括选择公理、命题外延性和商类型的可靠性原则。系统会将这些原则的使用记录为对公理的依赖，而不是将其隐藏在证明语法之中。(docs.lean-lang.org)
证明的构造与检查
用户可以直接编写证明项，也可以使用证明策略交互式地构造证明。证明策略是一种转换证明状态的程序，而证明状态由尚未完成的目标和可用的假设组成。常见操作包括引入假设、应用已有定理、利用等式改写表达式，以及简化目标。策略脚本最终会构造出证明项；它们本身并不是额外的逻辑推理规则。(lean-lang.org)
例如，以下 Lean 4 声明证明了一个命题蕴含其自身：
theorem identity_implication (P : Prop) : P → P := by
intro h
exact h
其中，intro h 引入作为假设的 P 的证明，而 exact h 则将该证明用作结论的证明。相应的直接证明项是 fun h => h。更复杂的证明可以将显式给出的中间命题与自动化工具结合起来，例如使用 simp 根据定理进行化简。(lean-lang.org)
在检查之前，精化过程会将便于书写的表层语法转换为显式的核心表达式。它会补全省略的参数，解析重载记号，处理强制类型转换，以及其他根据上下文推断的信息。随后，内核会独立于这些推断过程检查声明。这种分离限制了前端或证明策略中的错误所能造成的影响：错误构造的普通证明项应当被内核拒绝。(lean-lang.org)
编程与数学库
Lean 4 将函数式编程与开发实用可执行软件所需的功能结合起来。其可扩展性允许用户编写元程序，以操作表达式并实现专门的自动化功能。类型类用于组织可复用的接口，并支持自动选择实例，其中也包括解释数学记号所需的代数结构。Lean 的构建与包管理工具 Lake 用于组织项目、依赖项、库和可执行程序。(lean-lang.org)
社区的主要数学库是 Mathlib。它包含定义、定理、编程基础设施和证明策略，涵盖代数、线性代数、拓扑学、数学分析和测度论等领域。其共享的结构层级允许在可复用的假设下陈述结果，而不必为每个数学领域独立重建相关基础。贡献者须遵循社区在命名、风格、文档和审查方面的规范。(github.com)
适用范围与信任边界
Lean 检查的是实际编码的形式化陈述，而不是该陈述是否忠实表达了作者的非形式化意图。因此，通过检查的证明表明，相应结论可以从所采用的定义和假设中推导出来；如何理解这些定义，仍是另一项任务。这一区别在数学形式化和软件规格验证中都很重要。(leanprover-community.github.io)
成功处理一个文件，也不足以证明其中每个定理都有完整的证明。占位符 sorry 使用 sorryAx，而后者可以构造任意类型的项。Lean 的 #print axioms 命令能够显示直接和间接的公理依赖。依赖原生求值的证明还依赖编译后的计算，因此其信任边界超出了普通内核检查的范围。这些区别将完整且经过内核检查的证明，与尚未完成的声明或依赖额外假设的结果区分开来。(lean-lang.org)