Lean 4 是什么

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

一个系统，两个身份

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

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

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

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

两者用同一套语言、同一个类型检查器。def 与 theorem 在底层是同一个东西——后者只是「类型是命题」的前者。这一点在第 2 部分会彻底讲清。

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

安装：elan

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

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

Windows PowerShell：

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

装完验证：

lean --version

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

leanprover/lean4:v4.32.1

这解决了 Lean 生态的一个现实问题——Mathlib 紧跟新版本，而你的老项目可能停在旧版本。有了 elan，两者可以共存。

编辑器

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

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

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

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

项目：lake

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

新建项目：

lake new myproject

cd myproject
lake build

生成的结构：

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

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

lake new myproject math

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

lake exe cache get

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

三种运行方式

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 的差异化优势：

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

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

它被用在哪

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

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

-- 定义一个函数
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 一个定理，看到的是它证明了什么。

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

下一篇：第一个程序与第一个证明。

本页目录