# Lean 4 是什么

> 双重身份、elan 与 lake 工具链、装上就跑，以及与 Coq/Agda/Isabelle 的定位差异。

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/what-is-lean
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

## 一个系统，两个身份

Lean 4 既是**依值类型的函数式编程语言**，也是**交互式定理证明器**。

```lean
-- 身份一：编程语言。这是一个能跑的程序
def greet (name : String) : String :=
  s!"Hello, {name}!"

#eval greet "Lean"    -- "Hello, Lean!"
```

```lean
-- 身份二：定理证明器。这是一个被机器检查过的证明
theorem add_zero_eq (n : Nat) : n + 0 = n := by
  rfl
```

两者**用同一套语言、同一个类型检查器**。`def` 与 `theorem` 在底层是同一个东西——后者只是「类型是命题」的前者。这一点在[第 2 部分](https://daiw.org/manual/lean4/propositions-as-types)会彻底讲清。

Lean 自身的很大一部分（包括编译器前端与几乎全部 tactic）**是用 Lean 写的**——这是它与其他证明器的一个显著区别，也让元编程成为一等能力。

## 安装：elan

**不要直接装 Lean 二进制**，装 `elan`——它是 Lean 的版本管理器（对应 Rust 的 rustup）：

```bash
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
```

Windows PowerShell：

```powershell
irm https://elan.lean-lang.org/elan-init.ps1 | iex
```

装完验证：

```bash
lean --version
```

`elan` 的价值：**每个项目可以用不同的 Lean 版本**。项目根目录下的 `lean-toolchain` 文件写明该项目要哪个版本，`elan` 自动切换并按需下载。

```text
leanprover/lean4:v4.32.1
```

这解决了 Lean 生态的一个现实问题——[Mathlib](https://daiw.org/manual/lean4/mathlib) 紧跟新版本，而你的老项目可能停在旧版本。有了 `elan`，两者可以共存。

## 编辑器

**VS Code + Lean 4 扩展**是事实标准。装完扩展后打开 `.lean` 文件，右侧会出现 **Infoview** 面板——这是 Lean 开发的核心界面：

- 光标停在任意位置，Infoview 显示**当前的证明状态**（有哪些假设、要证什么目标）。
- 错误与警告实时显示。
- `#check` / `#eval` 的输出也在这里。

<Callout type="info">
  **Lean 的开发体验高度依赖 Infoview。** 不看 Infoview 写证明就像闭着眼睛调试——你必须时刻知道「现在的目标是什么」。

  另一个选择是 Neovim + `lean.nvim`，功能对等。Emacs 的 `lean4-mode` 也可用。
</Callout>

## 项目：lake

`lake` 是 Lean 的构建工具与包管理器（Lean 自带，不用单独装）。

新建项目：

```bash
lake new myproject
```

```bash
cd myproject
lake build
```

生成的结构：

```text
myproject/
├── lakefile.toml       构建配置（较新版本用 toml，旧版是 lakefile.lean）
├── lean-toolchain      指定 Lean 版本
├── Main.lean           可执行入口
├── Myproject.lean      库的根模块
└── Myproject/
    └── Basic.lean
```

带 Mathlib 的数学项目用专门的模板：

```bash
lake new myproject math
```

它会把 Mathlib 加进依赖。**首次构建 Mathlib 需要很久**——所以要用缓存：

```bash
lake exe cache get
```

这条命令下载预编译的 Mathlib，把几小时的编译变成几分钟的下载。**做数学形式化必用**。

## 三种运行方式

```bash
lake build           # 构建整个项目
lake exe myproject   # 运行可执行文件
lake env lean File.lean   # 单文件检查（带项目依赖）
```

日常写代码基本不手动跑这些——编辑器扩展会实时检查。命令行主要用于 CI 与最终验证。

## 与其他证明器的定位

| | Lean 4 | Coq/Rocq | Agda | Isabelle/HOL |
| --- | --- | --- | --- | --- |
| 基础理论 | 依值类型论（CIC 变体） | CIC | Martin-Löf 类型论 | 高阶逻辑 |
| 也是通用编程语言 | **是**（有编译器，产原生代码） | 有提取 | 有，但少用于工程 | 否 |
| 元编程 | **用 Lean 写 Lean** | Ltac/Ltac2 | 反射 | ML |
| 主力数学库 | **Mathlib** | mathcomp 等 | 较小 | AFP |
| 数学社区活跃度 | **极高**（近年增长最快） | 高（偏 CS） | 中 | 中（偏形式化方法） |

**Lean 4 的差异化优势**：

1. **Mathlib 是目前最大的形式化数学库**，覆盖本科到研究生数学的广大范围。
2. **元编程用 Lean 自己写**——扩展语言不需要学第二套语言。
3. **是真正可用的编程语言**——有性能不错的编译器、引用计数内存管理、多线程支持。

代价是**变化快**：Lean 4 相对 Lean 3 是不兼容重写，且至今仍在快速演进。

## 它被用在哪

- **形式化数学**：Mathlib、Fields 奖得主参与的项目（如 Scholze 的 Liquid Tensor Experiment、Tao 的 PFR 形式化）。
- **软件验证**：编译器、密码学实现的正确性证明。
- **AI 定理证明研究**：Lean 是当前 AI 数学推理研究的主要目标平台——形式化的证明可被机器精确验证，这正是训练与评测所需要的。

## 一个「两个身份」的最小演示

```lean
-- 定义一个函数
def double (n : Nat) : Nat := n * 2

-- 它能算
#eval double 21        -- 42

-- 也能对它证明性质
theorem double_eq_add (n : Nat) : double n = n + n := by
  simp [double, Nat.mul_two]

-- 证明本身也是一个可以被引用的项
#check double_eq_add   -- ∀ (n : Nat), double n = n + n
```

注意最后一行：**定理的「类型」就是它所陈述的命题**。`#check` 一个定理，看到的是它证明了什么。

这就是接下来要展开的核心思想。

下一篇：[第一个程序与第一个证明](https://daiw.org/manual/lean4/first-steps)。