交互式定理证明简史
从 AUTOMATH 到 Lean 4 与计量先例
Lean 不是突然出现的「另一种 LaTeX」。它处在一条超过半个世纪的线索上：把数学证明写成可检查的形式对象，并用尽量小的内核保证推理合法。本页按这条线索走，最后落到与计量最相关的图书馆与先例。原理细节见 类型论与内核。
1 两条技术传统
Harrison 的综述把交互式定理证明（ITP, interactive theorem proving）分成若干重叠的传统 (Harrison 等 2014年)。对后来的 Lean 用户，记住两条主线即可。
类型论 / Curry–Howard 线。
1967 年起，de Bruijn 的 AUTOMATH（自动检查数学语言）把证明当作项来检查，是「证明即对象」的早期实现；1977 年已有人用它形式化 Landau 的分析基础。Martin-Löf 类型论、Coquand 的构造演算（CoC, Calculus of Constructions），以及后来的归纳构造演算（CIC, Calculus of Inductive Constructions），构成 Coq（现亦称 Rocq）与 Lean 的共同祖先。Curry–Howard 对应把「命题」与「类型」、「证明」与「程序」看成同一套结构，细节见下一篇。
LCF（Logic for Computable Functions，可计算函数逻辑） / HOL（Higher-Order Logic，高阶逻辑）线。
Scott 的可计算函数逻辑之后，Milner 的 Edinburgh LCF 引入关键工程思想：定理是抽象类型，只能由内核的少量规则构造；用户语言 ML（Meta Language，元语言）用来写策略（tactic，生成证明项的指令），策略再组合成大证明。HOL（Higher-Order Logic）家族（HOL4、HOL Light 等）与 Isabelle 主要由此生长。Paulson 后来把这段历史概括为「从 LCF 到 Isabelle/HOL」(Paulson 等 2019年)。
Lean 的逻辑更靠近 CIC（归纳构造演算），工程上却大量吸收了 LCF 的策略文化：用户写 by ...，系统生成证明项，内核检查项。
2 1970–2000：从实验到可用系统
粗线条时间表：
| 时期 | 事件 | 后来还在用的遗产 |
|---|---|---|
| 1967– | AUTOMATH（de Bruijn） | 证明检查、依赖类型 |
| 1970s | Edinburgh LCF、ML（Meta Language） | 小内核、策略、元语言 |
| 1973– | Mizar | 接近数学散文的形式语言 |
| 1980s | Coq / CIC（归纳构造演算） | 归纳类型、证明助手作为研究工具 |
| 1986– | Isabelle | 通用逻辑框架；1991 年起 Isabelle/HOL（高阶逻辑） |
| 1988– | HOL88 及后继 | 经典高阶逻辑、HOL Light 的极小内核 |
| 1990s | Proof General | Emacs 前端，统一「发送策略—看目标」 |
这一阶段的目标主要是：程序正确性与逻辑学本身。大规模「把分析教材搬进机器」还很少。Wiedijk 后来用 de Bruijn 因子（形式化文本长度相对人写数学的倍数）衡量代价：早期常见估计在一个数量级以上，目标是把它压到接近 1——即「写形式证明不要比写 LaTeX 难很多」。这个目标至今只在局部达到。
3 里程碑：计算机开始检查「真定理」
若干公开项目改变了数学家对形式化的观感。
- 四色定理（Coq）。 Gonthier 等把 Appel–Haken 以来依赖计算机穷举的证明，做成 Coq 检查的形式证明，展示「含大量计算的证明」也可以有内核证书。
- Kepler 猜想 / Flyspeck（HOL Light + Isabelle）。 Hales 等完成球堆积猜想的形式证明 (Hales 等 2017年)。问题本身曾因原始证明过长、含计算机部分而难以审稿；形式化提供了另一种审稿。
- Feit–Thompson 奇数阶定理（Coq）。 说明群论长证明可以团队化、工程化。
- 液态张量实验（LTE, Liquid Tensor Experiment；Lean 3 + Mathlib）。 2020 年 Scholze 公开挑战后，Commelin、Topaz 等在 2022 年完成液态向量空间主定理的 Lean 形式化 (Commelin 和 Topaz 2022年)。Buzzard 指出：几页人写证明对应数万行 Lean，往往是因为范畴论等基础设施当时还不在库里——库的厚度决定 de Bruijn 因子。
这些项目的共同教训，对计量同样适用：先有可复用库，再形式化「书上那一页」；陈述必须钉死；完成宣布的是某个形式陈述，不是口头上的整章教材。
4 Lean 本身
Lean 项目由 Leonardo de Moura 于 2013 年在微软研究院启动，系统描述见 CADE-25（Conference on Automated Deduction，自动演绎会议）2015 年论文 (Moura 等 2015年)。设计目标是同时服务数学形式化与系统验证，并把自动化放进可交互、可产生证明项的框架里 (Avigad 等 2025年)。
- Lean 2 / 3：Lean 3 时期社区建成 Mathlib（Lean 的数学库），吸引大量数学家。Kevin Buzzard 的 Xena 项目、Natural Number Game（NNG，自然数游戏），把入门从「读手册」变成「打关」。
- Lean 4（2021 年起逐步成为主线）：用 Lean 实现 Lean（自托管），元编程与构建系统 Lake（名称来自 Lean + Make）大幅加强。Mathlib 整体迁移为 mathlib4。社区明确建议不要再学 Lean 3 (Lean prover community 2025年)。
- 工具链钉死：每个项目一份
lean-toolchain，elan（Lean 工具链管理器）按文件安装对应版本。Mathlib 与 Lean 必须同标签，不能只升其中一个。
当前学习入口是社区的 Learning Lean 4 页：游戏、Mathematics in Lean（MIL）、Theorem Proving in Lean 4（TPIL）、The Mechanics of Proof、Functional Programming in Lean 并列，按口味选择 (Lean prover community 2025年)。
5 数学库改变了可行性
没有 Mathlib，形式化计量几乎要从 \(\sigma\)-代数写起。有了 Mathlib，条件期望、测度、线性代数、拓扑与部分概率极限定理是可引用的基础设施，代价是：
- 陈述比教材更一般（Bochner 积分、赋范空间、几乎处处）；
- 你必须写桥接引理（bridge lemma），把 Hansen 的记号接到库定理；
- 版本锁很严，复现别人的仓库要跟他们的
lean-toolchain。
这与实证里使用 R 包类似：你很少从 BLAS（Basic Linear Algebra Subprograms，基础线性代数子程序）写起，但必须理解包的假设，并且用锁文件固定版本。
6 2020s：教材、AI 与「第二通道」
近年三条并行发展与本栏目直接相关。
1. 教材式形式化。
把讲义或研究生概率课做成 Lean 伴侣，重点不是创新定理，而是对齐教学陈述与库接口。Deng 与 Shum 把这称为「教科书朝向的陈述 + Mathlib 桥」(Deng 和 Shum 2026年)。社区的 Hansen 项目 lean-hansen-econometrics 是同一思路在计量上的实例：先 inventory（定理清单），再证明，不逐句翻译正文。
2. 人机协作证明。
Terence Tao 等公开用 Lean 检查组合与分析论证；证明助手从「专家玩具」变成部分研究工作流。同时，自动形式化（把自然语言证明译成 Lean）仍不稳定：失败模式常常是译错定理而不是证错引理。
3. 大算力案例要当「解释课」而不是模板。
OpenAI 于 2026 年 9 月公布 Navier–Stokes（NS，纳维–斯托克斯）相关分析证明与 Lean 证书，对应 Clay 数学研究所千禧年问题表述中带光滑外力的 C/D，而不是无外力的 A/B；内核只检查形式陈述，Comparator（对照检查器）再对照独立问题陈述。本仓库方法页已写迁移表，见 参照仓库。计量评注不模仿上万并发智能体；要学的是：发现与核验拆开、陈述范围写死、第二通道对照原文。
7 计量与统计侧的公开尝试
相对代数几何与分析，概率统计的 Mathlib 覆盖更年轻，但已经不是空白：
- Mathlib 的
MeasureTheory/ProbabilityTheory：条件期望condExp、独立性、部分极限定理。 - lean-hansen-econometrics：Hansen《Econometrics》第 2–13 章有 Lean 模块（均为
partial，无一章标成整章完成），工具链钉在 Lean 4.29.0 与 Mathlib v4.29.0。 - 其他统计向仓库（如公开的 Statlean 类项目）尝试估计理论、中心极限定理（CLT, Central Limit Theorem）桥等，成熟度参差，引用前要看
sorry与公理表。
对我们的含义：Hansen 形式化是合理起点，因为教材定理编号稳定、线性代数与条件期望的核心已有库支持；渐近、自助法、弱工具则要更晚，且必须接受「教材一句话、Lean 一页假设」。
下一篇把历史落到逻辑：依赖类型、Curry–Howard 对应，以及 Lean 内核实际信任什么。