Lean 4 是一个基于依赖类型理论的定理证明器与编程语言，它将命题即类型（Propositions as Types）和证明即程序（Proofs as Programs）的 Curry-Howard 同构作为核心理念，实现了数学证明与可执行代码的统一 。
核心概念：命题即类型与证明即程序
在 Lean 中，每一个数学命题都被视为一个类型，而该命题的证明则是一个具有该类型的项（即程序）。这种对应关系构成了形式化验证的基础。
| 命题 P | 类型 P : Prop | 命题 P 本身是一个类型。 |
| 命题 P 的证明 | 项 h : P | 项 h 是类型 P 的一个实例，即 P 的一个证明。 |
| 蕴含 P → Q | 函数类型 P → Q | 一个从 P 的证明到 Q 的证明的函数。 |
| 全称量词 ∀ x, P x | 依值积类型 (x : α) → P x | 一个为每个 x 生成 P x 证明的函数。 |
| 存在量词 ∃ x, P x | 结构类型 Sigma | 包含一个见证 x 和其证明 h : P x 的对。 |
入门实践：环境配置与基本证明
1. 环境搭建
推荐使用 VS Code 配合 lean4 扩展进行开发。也可以通过 Gitpod 在线环境快速开始 。
2. 第一个证明：命题逻辑
以下代码展示了如何使用 Lean 证明一个简单的命题逻辑定理。
— 引入 Lean 的基本逻辑规则
import Mathlib.Tactic
— 定理：如果 P 成立，那么 P 或 Q 成立。
theorem or_intro_left (P Q : Prop) (h : P) : P ∨ Q := by
— `by` 关键字开始一个策略（tactic）证明块
— 目标：证明 P ∨ Q
— 已知条件 h: P
left — 选择证明左分支，即证明 P
exact h — 精确使用已知条件 h 来证明 P
在这个证明中：
- theorem 声明了一个定理 or_intro_left，它依赖于命题 P, Q 和一个 P 的证明 h。
- by 引导一个策略式证明。
- left 策略选择了析取命题 P ∨ Q 的左半部分 P 作为当前目标。
- exact h 策略指出，当前目标 P 恰好可以由假设 h 满足。
3. 使用数学库 mathlib4
mathlib4 是 Lean 庞大的社区数学库，包含了从基础代数到前沿拓扑学的大量形式化定义和定理 。使用 import 语句引入所需模块。
import Mathlib.Data.Real.Basic — 引入实数基本理论
import Mathlib.Topology.Basic — 引入拓扑学基本概念
— 利用 mathlib4 中的定理证明：两个连续函数的和是连续的
example {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
(f g : X → Y) (hf : Continuous f) (hg : Continuous g) :
Continuous (f + g) := by
— `Continuous.add` 是 mathlib4 中已证明的定理
exact Continuous.add hf hg
核心证明策略（Tactics）
Lean 的交互式证明主要通过策略（tactics）来完成。下表列举了最常用的核心策略 ：
| intro h | 引入假设。对于目标 P → Q，引入假设 h : P，新目标为 Q。 | 证明蕴含命题。 |
| apply h | 反向推理。如果 h : P → Q，且当前目标是 Q，则将目标变为 P。 | 使用已知定理进行推导。 |
| exact h | 精确匹配。用项 h 直接完成当前目标的证明。 | 当目标与某个已知证明完全一致时。 |
| rw [h] | 重写。根据等式或等价关系 h 改写目标或假设。 | 化简表达式或应用定义展开。 |
| simp | 自动化化简。使用库中的简化规则（如定义展开、计算）尝试证明目标。 | 处理包含简单计算的代数恒等式。 |
| induction n | 数学归纳法。对自然数 n 或其他归纳定义的类型进行归纳证明。 | 证明关于自然数、列表等递归结构的性质。 |
| use a | 构造存在量词证明。为 ∃ x, P x 提供见证 a，然后证明 P a。 | 证明存在性命题。 |
| cases h | 情况分析。对假设 h（如析取 h : A ∨ B）进行分情况讨论。 | 处理逻辑析取或归纳类型的构造子。 |
| have h' := … | 声明中间引理。在证明过程中推导出一个新的临时事实 h'。 | 分解复杂证明步骤。 |
策略证明实例：自然数性质
— 证明：对于任意自然数 n， n ≤ n^2 （当 n ≥ 1 时不成立，这里以 n=0,1 为例需讨论，此处展示策略流）
theorem le_square (n : ℕ) : n ≤ n * n := by
— 对 n 进行归纳
induction n with
| zero =>
— 基础情况: n = 0
simp — 0 ≤ 0 * 0 通过化简自动得证
| succ k ih =>
— 归纳步骤: 假设对于 k 有 ih: k ≤ k * k， 需证明 succ k ≤ (succ k) * (succ k)
— succ k 即 k+1
have : (k + 1) * (k + 1) = k * k + 2 * k + 1 := by ring
rw [this]
— 现在需要证明: k + 1 ≤ k * k + 2 * k + 1
— 根据归纳假设 ih: k ≤ k * k， 只需证明 1 ≤ 2*k + 1，这在自然数中显然成立
linarith [ih] — `linarith` 是用于线性算术的自动化策略
形式化数学的高级应用：拓扑学示例
Lean 和 mathlib4 能够处理高度抽象的数学概念。以下是一个拓扑学中“连续”定义的简单形式化及其证明 。
import Mathlib.Topology.Basic
— 定义：函数 f 在点 x 处连续（用滤子定义）
— 这里直接使用 mathlib4 中已形式化的定义 `ContinuousAt`
example {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
(f : X → Y) (x : X) : ContinuousAt f x := by
— 目标：根据连续的定义进行证明
— 展开 `ContinuousAt` 的定义（在交互环境中可用 `unfold ContinuousAt` 查看）
— 其核心是：对于 f x 的任意邻域 V，存在 x 的邻域 U，使得 f '' U ⊆ V
intro V hV — 引入 f x 的任意邻域 V 及假设 hV: V ∈ 𝓝 (f x)
— 需要构造 x 的一个邻域 U
— 在实际证明中，这里会根据 f 的具体性质（如多项式、连续函数等）进行构造
— 此处省略具体构造过程，仅展示框架
sorry — `sorry` 表示暂时跳过此证明，在完整形式化中必须被替换为有效证明
学习路径与资源建议
通过结合依赖类型论的坚实基础、强大的 mathlib4 库以及交互式的策略证明，Lean 4 为从初学者到专业数学家的用户提供了一个可靠且高效的数学形式化与验证环境 。
参考来源
- Lean 4定理证明实战教程
- 6个维度解析Lean 4：形式化证明与程序开发的双向革命
- Lean 4数学形式化：从基础定理到拓扑学的高级证明
- 如何使用 Lean 4 定理证明库：数学形式化的终极指南
- 形式化数学——Lean4
- 形式化数学——Lean4概述
