Lean 4 是 Lean 3 的后继版本，在设计目标、核心特性和性能上有显著改进。以下是两者的主要区别：
一、设计目标与架构
| 特性 | Lean 3 | Lean 4 |
|---|---|---|
| 目标 | 主要为交互式定理证明和形式化数学 | 扩展为通用编程语言，支持系统开发和高性能计算 |
| 架构 | 依赖外部 C++ 运行时 | 自托管（self-hosted），核心用 Lean 4 编写 |
| 编译目标 | 依赖外部工具链 | 直接编译为 C 或 LLVM，性能更接近原生代码 |
二、编程语言特性
| 特性 | Lean 3 | Lean 4 |
|---|---|---|
| 类型系统 | 依赖类型，但表达力有限 | 更强大的依赖类型，支持： - 高阶类型（Higher-Kinded Types） - 类型类（Type Classes）的钻石继承 |
| 纯函数式 | 强制纯函数式（除 unsafe 模块） | 支持纯函数式，但允许更灵活的副作用管理 |
| 宏系统 | 有限的宏支持 | 强大的编译期元编程，支持语法扩展 |
| 计算效果 | 通过 Monad 处理效果 | 引入更灵活的效果系统（如 IO、Except） |
三、包管理与生态
| 特性 | Lean 3 | Lean 4 |
|---|---|---|
| 包管理器 | 使用 elan + mathlib 仓库 | 内置 Lake 包管理器，支持依赖自动解析 |
| IDE 支持 | VS Code 扩展（功能有限） | 更完善的 VS Code 集成，实时类型检查和错误提示 |
| 标准库 | 较小，依赖 mathlib | 更全面，包含数据结构、算法和工具库 |
| 社区生态 | 主要用于学术和形式化验证 | 扩展到系统编程、Web 开发等领域 |
四、性能与可用性
| 特性 | Lean 3 | Lean 4 |
|---|---|---|
| 编译速度 | 较慢，特别是大型项目 | 显著提升（例如，mathlib4 编译速度比 mathlib 快 3-5 倍） |
| 运行时性能 | 依赖外部工具链，性能一般 | 直接编译为 C/LLVM，性能接近原生代码 |
| 安装与配置 | 复杂，需手动管理依赖 | 简化，Lake 自动处理依赖和环境配置 |
五、语法与编程体验
| 特性 | Lean 3 | Lean 4 |
|---|---|---|
| 语法 | 类似 Coq 和 Agda | 更接近 OCaml 和 Haskell，语法更简洁 |
| 交互式开发 | 基础的即时反馈 | 更强大的交互式环境，支持： - 实时类型检查 - 自动完成 - 错误定位 |
| 错误信息 | 有时不够友好 | 改进的错误信息，更易于理解和修复 |
六、示例对比
1. 类型类定义
Lean 3：
class Monad (m : Type → Type) :=
(pure : Π {α}, α → m α)
(bind : Π {α β}, m α → (α → m β) → m β)
Lean 4：
class Monad (m : Type u → Type v) where
pure : α → m α
bind : m α → (α → m β) → m β
2. 宏系统
Lean 4 中的宏示例：
syntax "hello_macro" term : command
@[commandElab hello_macro]
def elabHelloMacro : CommandElab
| `(hello_macro $e) =>
`(def hello := $e)
| _ => throwUnsupported
七、迁移与兼容性
- 代码迁移：Lean 4 与 Lean 3 不兼容，需要手动迁移代码。
- mathlib4：Lean 4 的数学库，从 Lean 3 的 mathlib 移植。
- 工具链：Lean 4 使用
lake替代leanpkg，依赖管理更简单。
总结：如何选择？
选择 Lean 3：
- 已有大量 Lean 3 代码，迁移成本高。
- 仅关注交互式定理证明，无需高性能或通用编程。
选择 Lean 4：
- 需要更好的性能和编译速度。
- 希望利用 Lean 作为通用编程语言（如开发工具、系统组件）。
- 愿意接受新语法和特性，参与社区发展。
Lean 4 是 Lean 语言的未来方向，其设计更现代、性能更优，适合新开发的项目。而 Lean 3 仍可用于维护现有代码库。