符号与连接
( thoughts-on :math )

机器如何读证明：Lean 与数学的形式化

|数学 & 形式
机器如何读证明：Lean 与数学的形式化——文章主题配图
( cover : ai-generated ) — 配图由 AI 生成

"AUTOMATH is a language intended for expressing detailed mathematical thoughts. … The rules are such that a computer can be instructed to check whether texts written in the language are correct." ——N. G. de Bruijn，1968 年技术报告 (de Bruijn, 1968)

"Automath 是一门用于表达细致数学思想的语言……其规则使得我们可以指令一台计算机，去检查用该语言写下的文本是否正确。"

引言

1998 年 8 月，托马斯·黑尔斯（Thomas C. Hales）与塞缪尔·弗格森（Samuel Ferguson）宣布借助计算机证明了开普勒猜想（Kepler conjecture）。随后的审稿成了一场马拉松：期刊为此指派了十二人的审稿小组，审了数年，直到审稿人精疲力竭、全体退出；距投稿近八年后，证明全文才得以发表，且是在未获审稿人完全认证的情况下发表的 (Hales, 2024)。审稿方留下的结论颇能说明问题——他们对"证明方法的本质正确性具有高度确信"，但确信不等于逐行核对 (Hales et al., 2017)。这场审稿的奇特之处在于，它并非制度的失灵，而恰是制度尽力的结果：十二位专家数年的工作，产出的仍然是"确信"，而不是"认证"。

另一类困境出现得更早。1976 年，阿佩尔（Kenneth Appel）与哈肯（Wolfgang Haken）借助计算机完成了四色定理的证明，期刊论文于次年发表 (Appel & Haken, 1977)。证明里由机器执行的那部分计算，人类审稿人无法用纸笔重演；对它的信任，只能寄托在对程序与人工整理的双重信任上。由机器完成的那部分论证，究竟该如何核验？

两件事指向同一处：数学证明的规模与计算含量，正在逼近人类审阅能力的上限。于是有了一个朴素的想法：既然证明越来越难被人读完，能不能让机器来读？不是让机器算数值，而是让机器逐条核对推理的每一步。把数学文本写成机器可逐行检查的形式语言，这项工作称为形式化（formalization）；为此发展出的软件，统称交互式定理证明器（interactive theorem prover）。形式化之后，一个证明的地位不再取决于"审稿人通读并信服"，而取决于一次可以无限重复的机械检查——这正是本文标题所说的"机器读证明"。

本文介绍这一领域及其最新代表 Lean。全文安排如下：第一章回到起点，从《数学原理》与希尔伯特纲领讲到 Automath、QED 宣言与四个已载入史册的形式化里程碑；第二章梳理证明器的技术谱系，交代 Coq、Isabelle、HOL 与 Lean 各自的来路；第三章拆解 Lean 的实现原理；第四章演示如何写下第一份机器检查的证明；第五章进入一个完整的形式化案例研究；第六章讨论人工智能与形式化的交汇；第七章清点这项事业的代价与限度；第八章给出可以上手的学习路径。

一、形式化的百年愿景

《数学原理》：手工形式化的极限

怀特海（Alfred North Whitehead）与罗素（Bertrand Russell）合著的《数学原理》（Principia Mathematica）是形式化理想的第一座纪念碑。三卷本于 1910、1912、1913 年由剑桥大学出版社出版，1925 至 1927 年刊行第二版 (Whitehead & Russell, 1910–1913)。这部书要做的事，是在一套人工符号语言内部，从极少的概念与公理出发，把算术与分析的命题逐条推演出来——每个中间步骤都写明依据，不依赖任何直觉。

书中流传最广的细节，是加法登场之晚。第一卷第 379 页的命题 ＊54.43 写道："From this proposition it will follow, when arithmetical addition has been defined, that 1 + 1 = 2."（待算术加法定义之后，由本命题将可推出 1+1=2。）真正的证明出现在第二卷第 86 页的命题 ＊110.643；紧跟证明，作者补了一句著名的评注："The above proposition is occasionally useful."（上列命题偶尔有用。）(Whitehead & Russell, 1910–1913)。坊间"用几百页证明 1+1=2"的段子需要修正：第 379 页处的只是预告，彼时加法尚无定义，正式证明在第二卷。但段子背后的印象并无大错——为了给"1+1=2"这样的平凡事实以无懈可击的根据，《数学原理》铺设的符号机器确实庞大得惊人。

《数学原理》证明了手工形式化在原则上可行，也证明了它在实践上不可行：没有人能以这种方式日常做数学。但它的真正遗产不在结论而在示范：当推理被写成纯粹的语法操作，"对错"就成了可以从外部判定的事，而无需诉诸推理者的权威与品味。这为后来的机器检查预留了全部接口——缺的只是一台机器，和一门为机器设计的语言。

希尔伯特纲领与哥德尔的界限

1920 年代初，希尔伯特（David Hilbert）提出后来以他命名的纲领：将全部数学公理化、形式化，并用"有穷"（finitary）方法证明这套形式系统的一致性 (Zach, 2023)。这与《数学原理》的努力方向一致，而目标更进一层：形式系统自身也要成为数学对象，其可靠性要在系统之内用最保守的手段确立。

1931 年，哥德尔（Kurt Gödel）发表论文《论〈数学原理〉及有关系统的形式不可判定命题》（Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I）——标题本身便点出了批判的靶子 (Gödel, 1931)。用《斯坦福哲学百科全书》条目的总结说，这项工作"一般被认为表明希尔伯特纲领无法按原样实施"（"Gödel's work is generally taken to show that Hilbert's Program cannot be carried out."）(Zach, 2023)。

本文的立场是：不完全性定理限定的是纲领的宏大版本——为全部数学一劳永逸地自证一致性；它并未禁止另一件事，即把一篇篇具体的证明写成可机械检查的形式对象。领会这一点的一个方式，是把"数学基础"与"具体证明的可靠性"分开：前者关心整座大厦的地基，后者关心每一块砖是否砌实。哥德尔定理动摇的是前一种抱负；形式化事业此后始终在第二种意义上工作，且卓有成效——机器核对不承诺元数学层面的终极安全，只承诺：若翻译忠实、核心无误，则证明链中不存在任何未经检验的推理步骤。

德布鲁因与 Automath：证明检查器的诞生

把形式化从哲学议题变成工程现实的，是荷兰数学家德布鲁因（N. G. de Bruijn）。1967 年前后，他开始构想"数学证明的形式检查器" (Geuvers & Nederpelt, 2022)；1967 至 1968 年，Automath 在埃因霍温理工大学（Technological University Eindhoven）成形，1968 年 11 月的技术报告（编号 T.H.-Report 68-WSK-05，49 页）是系统的首次完整陈述 (de Bruijn, 1968)。格弗斯与内德佩尔特在综述中称 Automath 为"第一个实际运转起来的定理证明器"（"the first theorem prover actually working"）(Geuvers & Nederpelt, 2022)。

德布鲁因对系统的定位说得清楚：Automath 用于表达细致的数学思想，其规则保证计算机可以被指令去检查文本的正确性（即本文题记）。这里出现了一个贯穿全部证明器历史的概念区分：证明检查器（proof checker）不同于定理证明器（theorem prover）。以这一区分回看，格弗斯与内德佩尔特笔下的"theorem prover"是当年的通行旧称，Automath 所做的正是证明检查。机器不负责发现证明——发现的智力负担仍在人类；机器负责的是核对，把"每一步推理是否合法"的检查从人手中接过来。这项分工看似谦逊，实则根本：核对的机械化意味着，判断一步推理是否合法不再依赖审阅者的学养与耐心，而变成规则的机械执行；在 1968 年，发现的机械化无从谈起，核对的机械化却已经可行。

Automath 的试金石是兰道（Edmund Landau）的教科书《分析基础》（Grundlagen）。范·本瑟姆·尤廷（L. S. van Benthem Jutting）把全书逐条翻译成 Automath，1976 至 1977 年间以博士论文《在 Automath 系统中检查兰道的〈分析基础〉》（Checking Landau's "Grundlagen" in the Automath system）完成并出版 (van Benthem Jutting, 1977)。第一次有一部数学教科书被完整形式化：公理、定义、定理、证明，无一例外。Automath 的遗产后来汇为 1024 页的文献汇编《Selected Papers on Automath》(Nederpelt, Geuvers & de Vrijer, 1994)。

QED 宣言：把全部数学装进系统的野心

1994 年，QED 宣言以论文形式刊于当年的自动演绎会议 CADE-12 论文集。它给项目的定义是："建造一个计算机系统，以切实表示全部重要的数学知识与技术"（"a project to build a computer system that effectively represents all important mathematical knowledge and techniques"）；宣言开篇便自陈，QED 只是这一项目"非常初步的暂定名称" (QED 项目, 1994)。全部数学——这个目标之宏大，与 Automath 当年一卷《分析基础》的谨慎恰成对照，但它把问题从此钉在了社区的议程上。

宣言之外，两条更早起步的道路已在各自积累机器可检查的数学。其一是 Mizar，由 Andrzej Trybulec 于 1973 年创立：关于 Mizar 思想的首次公开表述，是 1973 年 11 月 14 日在华沙大学图书情报研究所的一次研讨班报告；项目先依托普沃茨克科学学会（Płock Scientific Society），自 1976 年起落户比亚韦斯托克大学 (Mizar Team, 2025)。到 2018 年综述统计时，其数学库 MML 已积累逾五万条定理、逾百万行代码 (Bancerek et al., 2018)。其二是 Metamath，由诺曼·梅吉尔（Norman Megill, 1950–2021）创建，主库 set.mm 收录数万条已证定理——官网横幅称"逾四万条证明"，同站 FAQ 又作"逾两万三千条定理"，两个口径并存（2024 年 11 月页面）(Metamath 社区, 2024)。这两条道路与宣言彼此独立，却指向同一件事：数学知识可以以机器可检查的形式逐步积累。这份积累此后流向何处？后文的主线在 Lean 一边，但还会在库、基准与比较口径等场合与这两条道路重逢。

四个里程碑：形式化证明了自己

到二十世纪末，工具渐次成熟，接下来轮到成果说话。四个案例值得单独立传（人力与时间的细账留待第七章）。

四色定理（1976 / 2005）。 阿佩尔与哈肯 1976 年借助计算机完成证明；两篇期刊论文《每个平面地图皆可四着色》之一（放电法）与之二（可约性，与 J. Koch 合作）刊于 1977 年的《伊利诺伊数学杂志》(Appel & Haken, 1977)。二十九年后，Georges Gonthier 与 Benjamin Werner 在 Coq 中完成了证明的形式化复核 (Knies, 2012)；Gonthier 随后在《美国数学会通讯》撰文报告这一工作 (Gonthier, 2008)。计算机辅助证明中由机器承担的那部分论证，由此整体落入另一个程序的检查范围——原先悬置于"信任程序"的那一半证明，与人工论证同置于逐条核对之下。

开普勒猜想与 Flyspeck 项目（1998 / 2014）。 审稿马拉松之后（见引言），证明论文 2005 年刊于《数学年刊》(Hales, 2005)，完整系列 2006 年出齐 (Hales & Ferguson, 2006)。黑尔斯随即将"用机器完全核验自己的证明"立为项目，即 Flyspeck；项目于 2014 年 8 月 10 日官方完成 (Hales et al., 2017)。规模数字出自项目自身的报告：证明脚本总计约五十万行代码，项目耗约二十个工作人年；所依赖的 HOL Light 内核"只有几百行代码"；项目报告并称，Flyspeck"可能创下验证项目代码行数的纪录" (Hales et al., 2017; Hales, 2024)。

Feit–Thompson 奇数阶定理（2012）。 2012 年 9 月 20 日 17 时 46 分，Gonthier 向合作者发出邮件："This is really the End."（这下真的结束了。）(Knies, 2012) 次年论文发表：十五位作者——均署名于微软研究院与法国国家信息与自动化研究所（Inria）的联合中心——超过六年的协作，在 Coq 中完成奇数阶定理（Odd Order Theorem）证明的完整形式化 (Gonthier et al., 2013)。规模统计同样来自项目组：十七万行代码，一万五千个定义，四千三百条定理；统计邮件的末行写着 "Fun—enormous!"（乐趣——巨大。）(Knies, 2012)

液体张量实验（2020–2022）。 2020 年 12 月 5 日，彼得·朔尔策（Peter Scholze）在 Xena 项目博客发出挑战帖，提议形式化 Clausen–Scholze 液体向量空间理论的主定理。他给出的理由在数学家笔下罕见地直白：2019 年他有大半年沉迷于这个证明，"几乎为之发狂"；这"可能是我迄今为止最重要的定理"，而"最好确定它是对的" (Scholze, 2020)。Lean 社区接下了挑战，项目由 Johan Commelin 领衔，朔尔策本人持续提供数学支持 (Mathlib 社区, 2022)。2021 年 5 月 28 日，论证中连朔尔策本人也没有把握的部分得到完整验证；他在半年总结帖中写道，交互式证明助手已经能在合理的时间跨度内形式化验证困难的原创研究，"我觉得这绝对疯狂"，并对主证明宣布"再无剩余疑虑"——同时自评实验"大概完成了一半" (Scholze, 2021)。2022 年 7 月 14 日，液体张量实验（Liquid Tensor Experiment）全部完成 (Mathlib 社区, 2022)。在作者看来，这是形式化角色的分水岭：从复核已完成的经典，走到为进行中的原创研究担保。

四个案例合观，形式化的价值可以归结为四条（以下为作者的综合，所据事实均见上文引注）。第一，绝对可靠：机器检查的是证明的全部推理链，而非抽样复核；朔尔策的"再无剩余疑虑"是这个价值最直接的表达。当然，"绝对"的边界要划清——它相对于一组被审计的内核代码与选定的公理而言，这个边界留待第七章细究。第二，协作规模：奇数阶定理的十五人六年、Flyspeck 的约二十人年，都建立在"一部分推理一旦检查通过，合作者即无需重复审读"的分工方式之上；人力的节省不在写证明，而在不必反复互相确信。第三，可复用知识库：形式化的成果不是一次性的验收记录，而是可以引用、组合、继续生长的库——一条被收录的定理带着完整的证明对象，引用它即继承其全部可靠性；QED 宣言的愿景正在 Mathlib 一类的工程中部分兑现（见第二章）。第四，人工智能的基础设施：机器可检查的数学文本，同时是可以供机器检索与学习的环境；当证明以可检查的形式存在，"机器生成、机器验证、人提问并把关"便构成一条完整的闭环。这一点近年开始兑现，第六章再谈。

二、证明器谱系：Coq、Isabelle、HOL 与 Lean

两条路线：命题即类型，与小内核

今天的交互式定理证明器，大致可以按证明的载体分为两条路线。

第一条路线的思想核心是 Curry–Howard 对应（Curry–Howard correspondence），通行的口号是"命题即类型"（propositions as types）。哈斯凯尔·柯里（Haskell Curry）1934 年在组合逻辑的工作中观察到命题与类型之间的对应 (Curry, 1934)；W. A. 霍华德（W. A. Howard）1969 年完成手稿《公式即类型的构造观念》，1980 年正式发表 (Howard, 1980)。沃德勒（Philip Wadler）的概括常被引用：这一对应"由柯里在 1934 年观察到，由霍华德在 1969 年精炼" (Wadler, 2015)。在其现代形态里：每个命题是一个类型，该命题的证明是类型为它的一个项（term）——证明即程序；检查证明，就是检查项的类型。证明项（proof term）由此成为可存储、可传递、可组合的一等数据，一条定理的证明可以被另一条证明直接引用，如同程序调用库函数。沿这条路线的系统建立在依值类型论（dependent type theory）之上——"依值"指类型可以依赖于值（这一表达能力的意义，第三章细说）——代表是 Coq/Rocq、Agda 与 Lean。还有一层史实：格弗斯与内德佩尔特在综述中把 Automath 与后来的 Coq 并举，说后者与它一样建立在依值类型论与"命题即类型"原则之上 (Geuvers & Nederpelt, 2022)；而 Automath 对类型与命题的平行处理，实践上早于霍华德——系统于 1967 至 1968 年成形（第一章），霍华德的手稿次年才完成、公开发表更要等到 1980 年。

第二条路线源自 LCF。据戈登（Mike Gordon）的权威史料，最初的 LCF 系统是米尔纳（Robin Milner）1972 年在斯坦福大学开发的证明检查程序 (Gordon, 2000)；"LCF"之名则来自斯科特（Dana Scott）1969 年构想、1993 年才正式发表的可计算函数逻辑 (Gordon, 2000)。定型于 1979 年专著的爱丁堡 LCF 确立了影响至今的架构：米尔纳为此设计了程序语言 ML，其严格类型系统支撑起抽象类型（abstract type）机制，"以保证定理安全"——定理值只能由内核实现的推理规则构造，系统内任何用户代码都无法伪造一条定理 (Gordon, 2000; Gordon, Milner & Wadsworth, 1979)。"小内核、定理不可伪造"由此成为与依值类型并立的另一条传统。高阶逻辑（higher-order logic）证明器家族 HOL 由戈登 1980 年代初在剑桥奠基 (Gordon, 2000; Harrison, 2026)，1988 年前后成型的版本通称 HOL88，1993 年的专著是其权威文献 (Gordon & Melham, 1993)。Isabelle 则于 1986 年由保尔森（Lawrence C. Paulson）问世 (Paulson, 2026)，今日最常用的配置是高阶逻辑之上的 Isabelle/HOL；Makarius Wenzel 为其设计了声明式证明语言 Isar（Intelligible semi-automated reasoning，可读的半自动推理），以人类可读的证明文档为目标 (Wenzel, 1999)。

两条路线殊途同归的一点，是信任的集中：无论证明的最终载体是类型论内核的类型检查，还是抽象类型保护的定理对象，全部可信度都收拢到一小段可以独立审计的核心代码上——内核小到可以被人通读，第一章引过的 HOL Light 内核只有几百行，即是例证。差别在写法：前者以证明项为本，围绕类型的构造展开，用户直接或半自动地写出"类型为该命题的程序"；后者以目标驱动的证明策略（tactic）语言为本——屏幕上是一个待证目标，每条策略把它改写为一个或几个更简单的子目标，如此自顶向下，直至化归为公理与已有定理。两种写法在多数现代系统里可以混用，但证明的本体——证明项，或受保护的定理对象——界定了各家的血统。

四大系统速写

Coq（今名 Rocq）。 按项目官方史的记载：构造演算（Calculus of Constructions）的首个实现 1984 年由 Gérard Huet 与 Thierry Coquand 启动，实现语言是 INRIA 在 Rocquencourt 设计的 ML 系函数式语言 CAML；Coquand 于 1985 年给出构造演算的第一版；1989 年 Coquand 与 Christine Paulin 引入原始归纳定义，扩充为沿用至今的归纳构造演算（Calculus of Inductive Constructions）(Huet, Coquand & Paulin, 1995)。期刊论文见 (Coquand & Huet, 1988)。第一章的四色与奇数阶两大里程碑都是 Coq 的作品。2023 年末，项目公布更名计划，官网现为 rocq-prover.org；2025 年 3 月发布的 Rocq 9.0 起，编译器发行版全面应用新名 (Coq 团队, 2024)。

Isabelle/HOL。 保尔森 1986 年发布的通用证明框架 (Paulson, 2026)。旗舰成果之一是 seL4 微内核：Gerwin Klein 等十三人 2009 年发表的操作系统内核，第一个具备完整功能正确性（functional correctness）证明的通用操作系统内核，证明在 Isabelle/HOL 中完成 (Klein et al., 2009)。2004 年创办的证明库 AFP（Archive of Formal Proofs）持续收录机器检查的证明 (AFP, 2026)。Flyspeck 项目中，驯服图（tame graphs）分类部分的形式化即由 Isabelle 承担 (Hales et al., 2017)。

HOL Light。 约翰·哈里森（John Harrison）对原 HOL 的精简重设计，官方说明称其逻辑核心比其它 HOL 系统简单得多 (Harrison, 2026)；哈里森 2009 年的综述论文是了解它的系统门径 (Harrison, 2009)。它是 Flyspeck 的主力系统；应用还包括英特尔处理器的浮点验证与亚马逊云服务的密码学大数运算库 s2n-bignum (Hales, 2024; Harrison, 2026)。

Agda。 初版（Agda 1）由 Catarina Coquand 用 Haskell 实现——这里需要点名：是哥德堡的 Catarina Coquand，而非 Coq 的 Thierry Coquand，两位是不同的研究者 (Agda 社区, 2026)。现行 Agda 2 自 2005 年动工，主要文献是 Ulf Norell 2007 年的博士论文 (Norell, 2007)。

Mizar 与 Metamath 的进路第一章已有交代，此处不再展开；在两大路线的叙事之外，它们提醒我们：机器可检查这一目标，允许不止一种实现哲学。

Lean：谱系里的新来者

按 Lean 官方与基金会时间线的表述，Lean 项目由 Leonardo de Moura 于 2013 年在微软研究院启动 (Lean 官网, 2026)；他此前曾在 SRI International 与微软研究院从事自动推理与定理证明研究 (Lean FRO, 2026)。仓库的首次提交在 2013 年 7 月，2014 年 6 月发布首个版本 0.1 (Lean FRO, 2026)。系统描述论文 2015 年 8 月发表于自动演绎会议 CADE-25，五位作者 (de Moura et al., 2015)；这篇论文在 2025 年获得 Skolem 奖 (Lean FRO, 2026)。

版本沿革：Lean 3.0.0 于 2017 年 1 月 20 日发布；Lean 4 自 2018 年 4 月动工，其自举重写在 2021 年的 CADE-28 论文中有正式描述——"Lean 4 is a reimplementation of the Lean interactive theorem prover (ITP) in Lean itself."（Lean 4 是用 Lean 自身对 Lean 交互式定理证明器的重新实现。）(de Moura & Ullrich, 2021) 首个正式稳定版 4.0.0 发布于 2023 年 9 月 8 日 (Lean FRO, 2026)。

组织沿革：de Moura 现任亚马逊云服务自动推理组的资深首席应用科学家；2023 年 7 月，他与 Sebastian Ullrich 共同创立非营利组织 Lean FRO（Lean Focused Research Organization），隶属 Convergent Research 体系 (Lean FRO, 2026)。

而 Lean 在数学社区地位的真正支柱，是 Mathlib。截至 2026 年 9 月：官方统计页记定理 287,112 条、定义 136,473 个；Mathlib/ 目录的 Lean 代码实测逾 232 万行；贡献者 772 人（官方统计口径；按 GitHub 提交作者计为 332 人）(leanprover-community, 2026)。这些数字的口径值得留意：定理与定义出自官方统计页，行数来自对源码的直接统计，贡献者数随认定宽严从三百余人到七百余人不等——引用形式化规模数据时注明口径与日期，是这一领域的诚实习惯。

职业数学家为何愿意投入？黑尔斯 2008 年在《美国数学会通讯》发表《Formal Proof》一文，2014 年又在 Bourbaki 讨论班作专题报告，是面向数学界最系统的两篇劝说 (Hales, 2008; Hales, 2014)；朔尔策 2020 年亲自发起液体张量实验，则把形式化带进了研究现场（第一章末已述其意义）。在作者看来，Lean 的位置因此特殊：一边是依值类型路线几十年沉淀的证明项技术与自举实现，一边是 Mathlib 把定理库、社区与工具链滚成同一个雪球；两者叠加，数学家驻足的成本降到了值得尝试的水位。

至于这台机器内部如何运转——一个证明项如何被构造、如何被检查、信任最终落在哪一段代码上——是下一章的主题。

三、Lean 的实现原理

打开 Lean 的机盖，会看到一条贯穿始终的设计主线：把定义、定理、证明一律收拢为同一种对象——项（term）；把「检查证明」压缩为「检查项的类型」；再把这件事交给一段尽可能小的内核。内核之外，elaboration 负责把人写下的半成品补全为完整的项，tactic 框架让人以交互方式指挥这场补全，工程层则让两百多万行级别的数学库可以日常使用。本章自上而下走一遍：先看逻辑骨架（宇宙、Π 与 Σ、归纳类型），再看项在机器里的样子（Expr 与环境），然后是信任的账本（内核、公理、独立检查器与可靠性缺陷的真实案例），最后是三段实现的内幕——elaboration、策略的元编程本质、定义性相等的工程处置，以及编译与缓存的工程侧面。

依值类型论的骨架：宇宙、Π 与 Σ

第二章介绍了 Curry–Howard 对应的思想，现在看它在 Lean 中的具体语法。按官方教程的表述，Lean 的形式基础是「构造演算（Calculus of Constructions）的一个版本，带有可数层非累积的宇宙与归纳类型」(Avigad et al., 2026)。

宇宙（universe）解决的是「类型的类型」问题：每个表达式都有类型，类型自身也是对象，于是也要有类型——这就需要一个层级：Type 0 : Type 1 : Type 2 : ……，无穷向上；Type 是 Type 0 的简写 (Avigad et al., 2026)。命题住在最底层：Prop 即 Sort 0，Type 即 Sort 1，Type 1 即 Sort 2，依此类推，Sort u 是统摄整个层级的记法 (Avigad et al., 2026)。通用函数须对各层类型都适用，于是常量可以携带宇宙参数（宇宙多态）；第四章将看到的 @Nat.rec 输出里的 Sort u_1，就是一个宇宙变元。这个类型论还有一个不可少的侧面：每个项都有计算行为，都支持一个范式化（normalization）的概念——类型论不是一套静止的符号，而是一套带演算规则的语法 (Avigad et al., 2026)。Prop 另有一条特殊规则：若 β : Prop，则无论 α 住在哪个宇宙，(x : α) → β 仍是 Prop——教程称之为 Prop 的非直谓性（impredicativity），并解释说这反映的是「Prop 是命题的类型，而非数据的类型」(Avigad et al., 2026)。

命题层与数据层的分野，在依值函数类型处显形。全称量词就是它：「∀ x : α, p 不过是 (x : α) → p 的另一种记法」，p 为命题时前者更自然 (Avigad et al., 2026)。依值类型论中的 Π 类型即此构造——元编程手册里，Lean 项层面的 forallE 构造子就被描述为「Π 类型或 Π 表达式，常写作 ∀ n : t, b」(Paulino et al., 2026)。于是一个 ∀ 命题的证明就是一个函数：任给 x : α，交回一个 p x 的证明。普通函数空间 α → β 是 β 不依赖 x 的特例，蕴涵 p → q 又是量词空约束的特例——同一个箭头，既是函数的类型，也是蕴涵与全称量词的类型；「命题即类型」由口号落实为语法。

「依值」二字的本义也在此处显形：类型可以依赖值。List α 依赖一个类型参数；而向量类型 Vector α n 连长度 n 也作为参数——同一个类型构造子，作用于不同的值，给出不同的类型。正是这一步让类型论的表达力越过简单类型论：既然类型里可以出现值，命题里就可以出现项，「对所有自然数 n，……」这样的断言才可能整体成为一个类型 (Avigad et al., 2026)。

对偶地，数据世界有依值对：Σ 类型 Σ a : α, β a。命题世界的存在量词 ∃ 在 Lean 中实现为命题层的一个归纳类型，其构造子 Exists.intro 恰是一个依值对——一半是见证，一半是「见证满足性质」的证明。教程的总结正点破这层关系：「存在命题与 Σ 类型非常相似……二者的相似是 Curry–Howard 对应的又一实例」(Avigad et al., 2026)。第四章会用一行 Exists.intro 0 rfl 演示。

最后一块基石是归纳类型（inductive type）。官方教程的表述近乎纲领：除了宇宙与依值箭头，库中每个具体类型都是归纳类型的实例；单凭宇宙、依值箭头与归纳类型这三样，即可立起数学的大厦 (Avigad et al., 2026)。归纳类型由一组构造子（constructor）定义，自然数是最经典的例子——zero 与 succ 两个构造子，Nat 是「由它们生成的最小类型」。而每个归纳定义都会自动获得一个消去子（recursor，又译递归子）：它把「定义一个从 Nat 到任意动机的依值函数」的需求，拆成 zero 情形与 succ 情形两份说明书；「归纳原理只是递归原理落在 Prop 上的特例」(Avigad et al., 2026)。这句话的分量——数学归纳法不是公理，而是构造的赠品——第五章展开。

项的表示：Expr 与环境

在实现层面，上述一切项共享一个数据类型 Expr。「Expr（类型的项）是 Lean 程序的抽象语法树：每个可以写出的项都对应一个 Expr」(Paulino et al., 2026)。它的构造子一望可知是一部 λ 演算的目录：约束变元 bvar、自由变元 fvar、元变量 mvar、宇宙排序 sort、常量 const、函数应用 app、λ 抽象 lam、依值箭头 forallE、局部定义 letE，另有三个次要构造子——字面量 lit（免得把一万写成 Nat.succ 的一万层嵌套）、元数据 mdata、投影 proj (Paulino et al., 2026)。

两处细节值得停留。其一，约束变元不记名字，记「德布鲁因索引」（de Bruijn index）——从变元向上数几层绑定器，便是它的归属；同名变元的捕获错误由此根除。这项技术正得名于第一章那位德布鲁因，半个多世纪后仍是实现的首选。其二，Prop 与 Type 在这一层并无神秘可言：Prop 就是 sort Level.zero，Type 是 sort (Level.succ Level.zero)；宇宙多态的常量则随身携带宇宙实参 (Paulino et al., 2026)。

还有一个方向上的翻译值得记下：match 模式匹配、do 块、by 块这些高层写法，在 Expr 中没有直接对应，「必须先被翻译成表达式——承担这项（可观）工作的部分就是 elaborator」(Paulino et al., 2026)。反过来，补全一旦完成，Expr 层的世界相当简单：手册提醒，「在 Expr 层，常量总是应用于其全部参数，无论隐式与否」(Paulino et al., 2026)——用户省略的每一个隐参，在这里都是显式的实体。

常量的含义存放在环境（environment）里。元编程手册的描述是：环境收录「编译器所需的全部信息——所有已知的声明，它们的类型、文档字符串、值等」(Paulino et al., 2026)。一个 Lean 文件是一串命令（def、inductive、structure、#check、#eval……），每条命令要么查询环境、要么扩充它 (Paulino et al., 2026)。所谓数学「库」，在实现层面就是环境的导入与累积：Mathlib 的 28.7 万条定理（截至 2026-09，第二章已引），是 28.7 万个可按名引用的环境声明。

内核与信任基

全部信任落在一段尽可能小的代码上：内核（kernel）。它的职责薄得可以用一句话说尽——「tactic 块结束后，Expr 被送往内核，由它检查这个项是否良构、是否真有所声称的类型」(Paulino et al., 2026)。既然证明即项、命题即类型，检查类型就是检查证明；第二章 LCF 传统里靠抽象类型守护的「定理不可伪造」，在 Curry–Howard 路线上由类型检查本身承担。也正因如此，手册补了一句安民告示：「tactic 的缺陷不是致命的：你写错了，内核最终会抓住它」(Paulino et al., 2026)——无论外层的自动化多复杂，出错面都收敛到这一小段检查器。

内核检查的主要计算内容，是定义性相等（definitional equality，社区简称 defeq）：「归约到相同值的两个项，被视为同一个」(Avigad et al., 2026)。rfl 是它的用户界面——库中把 rfl 定义为 Eq.refl _ 的记法，于是 2 + 3 = 5 一类的等式无须「证明」，两边算到同一形状即可 (Avigad et al., 2026)。defeq 的边界与代价，见本章第六节。

信任要可审计，须能回答两个问题：证明用了哪些公理？检查器自身可靠吗？第一个问题有现成命令：#print axioms 列出一条定理依赖的全部公理。标准环境中默认只有三条：命题外延性 propext（互相等价的命题相等）、商类型的可靠规则 Quot.sound（支撑 Lean 的商类型构造）、经典选择公理 Classical.choice（经典推理的来源）；教程第十二章对这三条逐一说明，并指明依赖它们的定理会在 #print axioms 中如实现身 (Avigad et al., 2026)——例如排中律 Classical.em 三条全依赖，而第四章将见到的 zero_add 一条也不依赖（本机 Lean 4.33.1 实测，2026-09）。公理逐条登记、逐条可查，第一章所说的「绝对可靠的边界」，在实现上就是这个清单。

第二个问题的答案是一个生态而非一个数字。内核之外存在独立实现：lean4lean 自述为「用（近乎纯）Lean 4 写成的 Lean 4 内核」，其论文标题本身就是立场——《Lean4Lean：用 Lean 验证 Lean 的类型检查器》，2025 年发表于 TYPES 会议 (Carneiro, 2024)。在作者看来，这个项目的意味比「又一份实现」更深一层：把检查器写成 Lean 程序，检查器的正确性也就成了可以交给机器检验的数学命题——信任的螺旋又收紧一圈。Lean 3 时代有 Scala 写成的 trepplein (Ebner, 2022)；另有 leanprover/tc 参考检查器。同一份证明数据交给不同代码库复核，审计就从「通读代码」变成「交叉验证」。

这道防线并非理论装饰。2026 年 8 月 18 日合入内核的一个修复（PR #14807）记录了真实的可靠性缺陷：is_prop 检查对经 whnf 归约后「卡住」且并非 Sort 的项错误地返回 false，由此绕过证明无关性（proof irrelevance）守卫，使一个被当作命题使用的值可被投影出数据字段，最终推出 False (de Moura, 2026)。同一个伪证还骗过了另一个独立实现 nanoda；PR 正文写道，「我们相信 lean4lean 外部内核没有这个缺陷」(de Moura, 2026)。同批另有两处 soundness 相关修复（#14806、#14843），均挂 soundness 标签。这件事的教益有三层：小内核不等于零风险；缺陷会被发现、公开并修复；而多实现交叉验证恰在此刻显出价值。第七章讨论限度时将回到这里。

Elaboration：把人写的一半补成机器要的全份

人写下的从来不是完整的项：隐参数省略了，类型省略了，记号是糖。用户面对的是具体语法树 Syntax，内核要的是抽象语法树 Expr；「elaborator 负责把用户面对的 Syntax 翻译成编译器其余部分可处理的东西——多数时候，这意味着把 Syntax 翻译成 Expr」(Paulino et al., 2026)。elaboration 一词本文保留原文，指的就是这个补全阶段。官方教程从用户一侧给出的定义同此：「把这些『洞』或『占位符』实例化的过程，通常就称为 elaboration」，并说 Lean 由此能推断函数类型、谓词乃至证明 (Avigad et al., 2026)。补全靠三件工具。

元变量（metavariable）是待填的洞——「表达式中等待日后填充的空洞」；同一对象换个视角就是证明界面的目标（goal）(Paulino et al., 2026)。#check (id) 输出中的 id : ?m.1 → ?m.1，那个 ?m.1 就是尚未确定的隐参在用户眼前的样子 (Avigad et al., 2026)。

合一（unification）负责把洞填上。判定两个表达式是否定义性相等的 isDefEq，遇到可赋值的元变量会顺势赋值——手册说「我们称 isDefEq 合一了这两个表达式」，例如 List ?m =?= List Nat 成功并把 ?m 赋为 Nat (Paulino et al., 2026)。合一并非蛮力：isDefEq 并不真正计算两边的范式——那太昂贵——而是「用尽可能少的归约去凑合两边」，本质上是启发式的工作，失手时可能变得很贵 (Paulino et al., 2026)。更深的坎在高处：等式替换一类的操作要求推断一个谓词隐参，这是高阶合一；「一般而论，判断高阶合一子是否存在是不可判定的，Lean 至多提供不完美且近似的解」(Avigad et al., 2026)。不可判定性没有挂在门口示警，它化在日常的启发式里。

第三件是合成元变量（synthetic metavariable）：为洞登记「应由何种机制解决」，共四类——typeClass（类型类解析）、coe（强制转换，类型类的特例）、tactic（交给一段策略）、postponed（暂缓，等更多信息）(Paulino et al., 2026)。类型类（type class）机制由此并入 elaboration 主循环：instance 声明注册的实现，在需要处被自动检索。信息不足时，elaborator 还可以挂起当前子问题、先处理别的，回头再续——教程以 List.foldr .add 0 [1,2,3] 为例演示了这场调度：.add 的含义须等到其他参数把类型信息凑齐之后才能确定；若信息最终仍不齐，elaboration 便以失败告终，报出「点记号无法解析」一类的错误 (Paulino et al., 2026)。

至此可以回答一个常见的困惑：term mode 与 tactic mode 是不是两种证明？不是。「陈述一个定理，概念上就是创建一个目标——构造一个具有期望类型的项」；凡写项之处都可换成 by 块，让一串策略逐段搭出这个项 (Avigad et al., 2026)。教程特意对照演示后用 #print 验证：更省事的 tactic 写法「产生完全相同的证明项」(Avigad et al., 2026)。两种模式是同一份内核对象的两副面孔，中间站着的那个翻译，就是 elaboration。

Tactic 即元程序：一种语言的自举

第二章的历史里，扩展一台证明器往往意味着再学一门语言：爱丁堡 LCF 为此发明了 ML；到今天，用元编程手册的对照表说，「在 Isabelle，元层语言是 ML 和 Scala；在 Coq 是 OCaml；在 Agda 是 Haskell。而在 Lean 4，元代码主要用 Lean 自身写成，少数组件用 C++」(Paulino et al., 2026)。这与 CADE-28 论文的自述——Lean 4 是「用 Lean 自身对 Lean 交互式定理证明器的重新实现」(de Moura & Ullrich, 2021)——互为表里：自举不只是一场工程表演，它把 tactic 框架从系统的特权子系统降格为一个库。

直接的后果是，写策略与写证明用的是同一门语言、同一个环境。手册的入门示例本身就在演示这件事：一行 elab 命令即可定义一个新的查询命令；一个十余行的定义即可写出一条名为 suppose 的自定义策略，其实现正是取当前目标、用 mkFreshExprMVar 造一个新的元变量、再把证明责任登记为新目标 (Paulino et al., 2026)——上一节「元变量即目标」的活例证 (Paulino et al., 2026)。手册还点出要害：「可以在我们执行对象层活动的同一个开发环境里，定义自定义语法节点并实现其 elaboration 例程……这一概念通常称为反射（reflection）：元层被反射到对象层」(Paulino et al., 2026)。宏系统与嵌入式 DSL 因此成为平常事：声明一个语法类别、给出几条宏规则，一门小语言就嵌进了 Lean——手册用不到一页搭出一个小型算术语言即是例证 (Paulino et al., 2026)。Mathlib 中那些领域定制的记号与策略，走的都是这条通道。

再往深处说一层（作者的综合）：扩展门槛的坍缩改变了生态的形状。证明语言的使用者与扩展者变成同一群人，库的贡献者因此同时贡献数学与工具；第二章引过的 772 人贡献者名单（官方口径，截至 2026-09）里，这两类工作早已无法拆开。第二章还说过，Milner为 LCF 设计 ML 是为了用类型系统「保证定理安全」；Lean 4 把这段历史收束成了同一个语言内部的分工——安全仍由内核独立守护，而扩展不再需要另一门语言。

定义性相等的工程学：透明度与弱头范式

defeq 是内核与 elaborator 共用的底层操作，而把项完全算到范式可以贵得离谱。Lean 的工程处置一横一纵。

纵向是透明度（transparency）：展开哪些常量，由四档开关决定——reducible（仅展开标了 @[reducible] 的常量，abbrev 即其简写）、instances（再加上 @[instance]，instance 即其简写）、default（展开除 @[irreducible] 外的一切）、all。动机说得很直白：「如果允许归约总是展开每个常量，类型类搜索一类的操作将贵得无法接受」(Paulino et al., 2026)。手册用一个层层嵌套的小定义演示：同一个常量，在四档开关下依次归约出四个深度不同的答案。同一个项在不同透明度下有不同的范式——「归约」从来是相对一档开关而言的。

横向是弱头范式（weak head normal form，whnf）：多数场合根本不必把项算到底。要判断一个假设的类型是否为 P ∧ Q，无须知道 P 内部是什么；对手册给出的这条判别函数，只消对整体做一次 whnf，再比对最外层的构造子即可，P 与 Q 内部一概不算 (Paulino et al., 2026)。「完全范式化的 reduce 事实上很少使用；Lean 归约的主力是 whnf」——把表达式归约到形如 f x₁ … xₙ、且 f 在当前透明度下无法再归约即停 (Paulino et al., 2026)。构造子应用、λ 表达式、Π 表达式、Sort 都是这样的停点。isDefEq「用尽可能少的归约凑合两边」，凑合的正是一个个 whnf。

工程侧面：编译、构建与缓存

作为一门完整的编程语言，Lean 有两条执行通路，官方教程一句话说尽：「它有一个生成二进制可执行文件的编译器，和一个交互式解释器」(Avigad et al., 2026)——编辑器里 #eval 的即问即答走解释执行，正式构建走编译。编译目标不是机器码而是 C：在本机新建一个最小项目并构建（Lean 4.33.1，2026-09 实测），lake 依次产出每个模块的 .c 文件、经系统 C 工具链编出的对象文件与可执行文件，以及供导入复用的 .olean 编译产物——后者连同 .hash 摘要一起，构成增量构建的凭据。构建日志里两条轨道并行可见：每个模块先报「Built」（产 olean），再报「Built …:c.o」（产 C 对象文件）——检查用的中间表示与执行用的本地代码，各自成链。

构建与依赖由 lake 打理（本机 Lake 5.0.0），工具链版本由 elan 按 lean-toolchain 文件自动选择与下载（本机实测，2026-09）——版本管理、包管理与构建就此闭环。这套机制的意义在 Mathlib 一端最直观：逾 232 万行 Lean 源码（第二章已引）无须任何人从零重编——仓库 README 的指引是先取预编译产物：lake exe cache get 下载由持续集成算好的 olean 文件，并注明「跳过这一步，下一步会非常慢」(leanprover-community, 2026)。缓存不是锦上添花：它决定了「单一的大库」这种组织形态在工程上是否成立。

机件至此拆完。但读图不等于会开车。下一章回到键盘前，把这些机制逐一踩在脚下。

四、Lean 语言入门：写第一个证明

本章换到动手的一侧。以下全部代码在本机 Lean 4.33.1（2026-09）编译验证通过——零错误，也没有任何占位证明；代码按讲解的顺序出自同一份验证脚本，信息行的输出逐字照录，读者不妨边读边在编辑器里复现。工具链的安装与项目搭建留待第八章，这里只看语言本身。

语法骨架：定义、定理与问询

一个 Lean 文件由命令组成，最常用的是声明：def「向工作环境声明新的常量符号」，inductive 声明归纳类型，structure 声明结构 (Avigad et al., 2026; Paulino et al., 2026)。向系统查询信息的辅助命令以井号开头 (Avigad et al., 2026)：#check 报告一个表达式的类型，#eval 对表达式求值；同一家族还有 #print，它显示一个声明的实际内容——教程正是用它查看策略式证明最终产生的证明项 (Avigad et al., 2026)。定理与定义共用同一套项语法——theorem 名称 : 命题 := 证明项；example 则是一条不留名的定理，适合练手。instance 声明类型类的实现，它就是打了 @[instance] 标记的 def (Paulino et al., 2026)。名称由命名空间（namespace）组织成层级，如 List.map、Nat.add (Avigad et al., 2026)。另有几件整理术：variable 声明的变量会自动插入引用它们的定义，section 与 namespace 限定声明的作用范围 (Avigad et al., 2026)。

第一份证明：1+1=2

lean
example : 1 + 1 = 2 := rfl
theorem id_prop {p : Prop} (h : p) : p := h

第一行是第一章那个著名的等式：在《数学原理》里，它的正式证明要等到第二卷；在这里是一行。rfl 交回的是自反性证明——库中把 rfl 定义为 Eq.refl _ 的记法，等式两边经定义性相等归约到同一形状，无须再做什么。教程提醒自反性比看上去强大：构造演算中的项有计算解释，共同归约到的项被视为同一个，于是诸如 (fun x => f x) a = f a、2 + 3 = 5 这样的非平凡恒等式也都由 rfl 直接证得 (Avigad et al., 2026)。第二行更有内容：h : p 把「p 的证明」本身当作一个变量，定理体原样把它交回——一个作用在证明上的恒等函数。命题即类型在这里不是比喻：h 就是一个普通的项，可以绑定、传递、复用。花括号 {p : Prop} 标记隐参，不必显式给出，由 elaboration 从上下文补全（第三章第四节）。

两种写法：term 与 tactic

官方教程对两种模式的分工有一段提纲挈领的描述：「证明项是数学证明的一种表示；tactic 是描述如何搭出这样一个证明的命令或指令」——非正式地讲，你开始一个证明时会说「先展开定义、再用引理、最后化简」，策略就是告诉 Lean 如何构造证明项的这类指令；它们天然支持增量式的写法，把证明拆开、一个目标一个目标地推进 (Avigad et al., 2026)。教程同时也点出代价与回报：策略式证明可能更难读，因为读者须预判每条指令的后果；但往往更短、更易写，而且「策略是通往 Lean 自动化的门径，因为自动过程本身就是策略」(Avigad et al., 2026)。

合取交换律的 term 写法：

lean
theorem and_comm' (p q : Prop) : p ∧ q → q ∧ p := fun h => ⟨h.right, h.left⟩

读法：fun h => … 是 λ 抽象——蕴涵的证明是函数；⟨h.right, h.left⟩ 是匿名构造子（anonymous constructor）记法，这里即 And.intro，其中 .left 与 .right 把假设 h 拆成两半再交换位置。整个项的类型恰是 p ∧ q → q ∧ p。

同一素材的 tactic 写法（命题换成当且仅当）：

lean
theorem and_comm_tactic (p q : Prop) : p ∧ q ↔ q ∧ p := by
  constructor
  · intro h; exact ⟨h.right, h.left⟩
  · intro h; exact ⟨h.right, h.left⟩

by 之后的每一行是一条策略。「陈述一个定理，概念上就是创建一个目标——构造一个具有期望类型的项」(Avigad et al., 2026)；策略逐条改写目标。constructor 施加「归纳类型的第一个适用构造子」(Avigad et al., 2026)——对双向蕴涵即 Iff.intro，目标应声裂为正向、反向两个。两个圆点「·」是分支符号，各自处理一个子目标 (Avigad et al., 2026)。intro 是「交互地构造函数抽象」的策略 (Avigad et al., 2026)——干的正是 fun h => 的活；exact 则把给定项整个填进目标，「它是 apply 的一个变体，表明该表达式应恰好填满目标」(Avigad et al., 2026)。而 apply 本身「把一个表达式当作多参函数施加：将它的结论与当前目标合一，并为余下的参数创建新目标」(Avigad et al., 2026)——想先用某条引理、再补它缺的前提时，用 apply；手里已有整份证明时，用 exact。族中还有一件懒人利器 assumption：它在当前目标的上下文里逐条翻找假设，「若有与结论相合者，便直接施用」，必要时还会顺手合一结论中的元变量 (Avigad et al., 2026)。填进两个分支的 ⟨h.right, h.left⟩ 与 term 版一字不差。须说准的是：本节两例命题有别（蕴涵对当且仅当），各自的内核项自然不同；教程在命题相同的同类对照后以 #print 验证过，那种情形下两种写法「产生完全相同的证明项」(Avigad et al., 2026)。第三章的论点在此落地——term 模式把证明项一次写就，tactic 模式逐段搭出，落进内核的都是项，差别只在你愿意亲手写多少。顺带一提工作方式：编辑器里把光标停在策略块内任意一行，窗口就会显示此刻的目标与上下文——证明是一步步看着目标长大的 (Avigad et al., 2026)。

rfl 的边界：为什么 0 + n = n 需要归纳

lean
example (n : Nat) : n + 0 = n := rfl
lean
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ m ih => rw [Nat.add_succ, ih]

core 中的加法对第二个参数递归——官方教程自建自然数时的定义即如此：固定 m，对 n 作递归 (Avigad et al., 2026)。于是 n + 0 是「已完成的计算」：按定义展开就是 n，rfl 收工；0 + n 却是「卡住的计算」：递归要向第二个参数询问形状，而 n 是未知数。对未知数成立的命题，路线只有归纳。induction n with 把目标交给 Nat 的消去子：zero 情形仍是 rfl；succ 情形中 ih : 0 + m = m 是归纳假设——消去子说明书里「已算出的前值」。rw [Nat.add_succ, ih] 两步走：先用库中引理 Nat.add_succ（类型为 n + m.succ = (n + m).succ）把目标 0 + (m + 1) = m + 1 的左端改写为 (0 + m) + 1，再用 ih 改写为 m + 1 = m + 1——rw 见到形如 t = t 的目标会自动以自反性闭合 (Avigad et al., 2026)。

数学家说这是「对 n 归纳」；类型论的描述更准确：这一步构造出的证明项，是消去子 Nat.rec 应用于动机 λ n => 0 + n = n 的两个分支——「归纳原理只是递归原理落在 Prop 上的特例」(Avigad et al., 2026)。同一枚消去子，动机落在 Type 里是递归地定义函数，落在 Prop 里是数学归纳法；官方教程在同类例子后补一句经验之谈——在这类证明中，rw 与 simp 往往非常有效 (Avigad et al., 2026)。第五章将看到这如何把皮亚诺第五公理一并吸收。

rw：等式替换的友好界面

lean
theorem two_step (n : Nat) (h : n + 0 = 0 + n) : 0 + n + 0 = n + 0 := by
  rw [Nat.add_zero, h]

rw 的机理是等式替换。原语是 Eq.subst：由 h₁ : a = b 与 h₂ : p a 构造 p b——「每个断言都尊重这个等价」(Avigad et al., 2026)。rw 是它的自动化包装：「用给定的等式——可以是假设、定理名或复合项——改写目标；若由此把目标化成 t = t，就自动施以自反性」(Avigad et al., 2026)。上面的两步是标准操作：先用库引理 Nat.add_zero 把左端化简（目标化为 0 + n = n + 0），再用假设 h 把右端替换成 0 + n，目标化为 0 + n = 0 + n，由 rw 自动闭合。方括号里可以列一串，rw [t₁, t₂] 即连改两次；←t 可反向使用等式；rw … at h 则改写假设而非目标 (Avigad et al., 2026)。

同一家族的自动化加强版是 simp：库中打了 [simp] 标记的恒等式被它「迭代地用于改写表达式中的子项」(Avigad et al., 2026)。教程的示例一望即知其用途：0 与 1 的常规恒等式，把 (x + 0) * (0 + y * 1 + z * 0) 一举化到 x * y。入门阶段记住分工即可：精确控制用 rw，交给常规化简用 simp。

消去子：归纳类型自带的说明书

lean
#check @Nat.rec
#print Nat.succ
#print axioms zero_add

本机输出，逐字照录：

@Nat.rec : {motive : Nat → Sort u_1} → motive Nat.zero → ((n : Nat) → motive n → motive n.succ) → (t : Nat) → motive t
constructor Nat.succ : Nat → Nat
'zero_add' does not depend on any axioms

第一行值得逐段读，它是每个归纳类型自动生成的说明书的标准样式 (Avigad et al., 2026)。开头是动机 motive : Nat → Sort u_1——要构造之物的类型族，宇宙变元 u_1 表明它对 Prop 与 Type 通用；随后两份小前提（minor premises）：zero 情形给出 motive Nat.zero，succ 步骤由 n 与 motive n（这正是归纳假设）造出 motive n.succ；末尾的大前提（major premise）t : Nat 是被消除的对象。教程还提到一个变体：Nat.recOn 与 Nat.rec 相同，只是把主前提挪到前面，而「在证明语境中使用时，它其实就是归纳原理的化装」(Avigad et al., 2026)。上一节 induction 生成的证明项，就是这两个分支加上主项。第二行显示构造子本体：Nat → Nat。第三行是第三章信任话题的现场：zero_add 零公理——rfl、归纳与 rw 的组合不引入任何公理；作为对照，经典逻辑的定理会如实申报依赖，如排中律依赖 propext、Quot.sound、Classical.choice 全部三条 (Avigad et al., 2026)。

存在量词与析取：构造子模式的复用

lean
example : ∃ n : Nat, n + 1 = 1 :=
  Exists.intro 0 rfl
lean
example : ∃ n : Nat, n + 1 = 1 := by
  exact ⟨0, rfl⟩

第三章说过，∃ 是命题层的依值对：Exists.intro 0 rfl 的两个参数正是「见证」与「见证合规的证明」；匿名构造子 ⟨0, rfl⟩ 是同一构造子的记法糖 (Avigad et al., 2026)，term 与 tactic 两种写法再次合一。反方向也有对偶的消去规则 Exists.elim：从「存在」中取出见证继续推理，其用法与 match 模式匹配同构——这又是 Curry–Howard 对应在语法上的显形 (Avigad et al., 2026)。要在策略模式下显式给出见证，core 提供的是 exists；Mathlib 一系另有功能更强的 use，如 use 5 / 2（本机 core 4.33.1 实测并无 use，它随 Mathlib 生态进入环境）(Avigad & Massot, 2026)。

析取则演示 cases：

lean
example (p q : Prop) (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

Or 有两个构造子 inl 与 inr；cases 用于「分解归纳类型的元素」(Avigad et al., 2026)，对双构造子的类型即分情况讨论，with 语法为每个分支命名。两个分支里 exact 各自填入对面的构造子——析取的交换成了两行的搬运。cases 的适用范围不限于命题：同一个策略也能对自然数分零与后继两情况，因为它们与 Or 一样，都是归纳类型 (Avigad et al., 2026)。

Mathlib：单一的大库，与它的检索方式

以上示例刻意只用 core，不依赖任何库；真实的证明工作则站在 Mathlib 之上。按其仓库自述，Mathlib 是「Lean 定理证明器的用户维护库，既包含程序基础设施，也包含数学，还包含使用前者、发展后者的策略」(leanprover-community, 2026)。规模第二章已引（截至 2026-09，约 28.7 万条定理）；组织形态是单一的标准大库——陶哲轩在形式化《Analysis I》之后评论，Lean「尤其是它『单一标准化库』的 Mathlib 模式，更贴合工作数学家实际的书写与思考方式」(Tao, 2025a)。

对入门者，Mathlib 的第一课是先查再证。后继非零是皮亚诺体系里第一个非平凡的事实，core 里已经有：

lean
#check (Nat.succ_ne_zero)
Nat.succ_ne_zero : ∀ (n : Nat), n.succ ≠ 0

查库常比自证便宜，也往往更好。检索不止一条路。让机器代查：本机实测对目标 0 + n = n 运行 apply?，Lean 给出的建议正是 exact Nat.zero_add n——上一节亲手证的那条定理，库里早有；exact? 则从「直接闭合目标」的方向搜索（两者都在 core 中）。按签名检索：社区维护的 Loogle 按类型模式搜索 Lean 与 Mathlib 的定义与定理 (Loogle, 2026)。翻阅文档：Mathlib 的文档站由 doc-gen4 从源文件自动生成，定理的命名有成文的约定可循 (leanprover-community, 2026)。而读签名本身是基本功——《Mathematics in Lean》的教法，就是用 #check 逐条检视库引理的类型，再以 apply 与 exact 组装成证明 (Avigad & Massot, 2026)。此外，README 明白写着：围绕 Mathlib 的讨论大部分发生在 Zulip 聊天室，欢迎加入或只读，各水平的提问都受欢迎 (leanprover-community, 2026)——对一个数学库来说，把求助渠道写进 README，本身即是一种姿态。

入门最平缓的路线另有其处：社区维护着以游戏关卡形式教学的 Natural Number Game，从零开始把本章的概念走一遍 (Buzzard & Eugster, 2026)；入口与整套学习路径，第八章统一给出。

至此，语言的骨架、证明项与策略的配合、库的位置都已就位。在作者看来，本章真正要带走的只有一件事：屏幕上的目标、策略改写的每一步、最终送进内核的那个项，是同一个对象的三种投影——理解了这一点，其余的都是查表。但入门示例终究是玩具。下一章把这架机器开进一部真实的教科书：以陶哲轩《Analysis I》为底本，看皮亚诺公理如何在 Lean 中一条条落地——看「公理」如何变成「定理」。

五、案例研究：《Analysis I》与皮亚诺公理的 Lean 实现

前四章的机器是空载运行的：概念虽真，示例皆为零散玩具。本章装上货物。以陶哲轩（Terence Tao）的教材《Analysis I》为底本，把它第 2 章的皮亚诺公理体系逐条放进 Lean，观察一个数学理论的最底层如何在类型论中重新奠基。选这部书作案例，理由有三：其一，它的起点比几乎全部同类教材都低——从皮亚诺公理出发构造整个数系，正好把形式化的地基暴露无遗；其二，作者本人维护着一份完整的 Lean 配套仓库，教材与代码可以逐条对照，而不是靠第三方的转述；其三，皮亚诺公理足够小，小到可以逐条讲完，又足够深——第五条公理恰好落在第三章讲过的那台核心机制上。

一部从零开始的教材

先说书。《Analysis I》是陶哲轩的实分析入门教材，属 TRIM 丛书（Texts and Readings in Mathematics）第 37 卷，由 Hindustan Book Agency 与 Springer 联合出版；初版 2006 年 1 月，第 2 版 2009 年，第 3 版 2015 年（Springer 版 2016 年），现行第 4 版 2022 年，Springer 电子版 2023 年 2 月上线 (Tao, 2022)。它的前身是 2003 年陶哲轩在加州大学洛杉矶分校（UCLA）一门荣誉课程的讲义，作者自述成书即该讲义的「扩充与清理版」(Tao, 2022)。

全书十一章加两个附录，目录本身就是一条构造路线 (Tao, 2022)。第 1 章导言之后是四章地基：第 2 章「从头开始：自然数」（Starting at the Beginning: The Natural Numbers），依次是皮亚诺公理、加法、乘法；第 3 章集合论，从元素与集合的基始讲起，罗素悖论与基数比较也在这一章；第 4 章整数与有理数；第 5 章实数。随后是分析本部：第 6 章序列的极限、第 7 章级数、第 8 章无穷集合、第 9 章实函数的连续性；收官两章是第 10 章微分与第 11 章黎曼积分。两个附录补外围：附录 A 数理逻辑基础，附录 B 十进制表示 (Tao, 2022)。

四章地基的分工一望即知：第 2 章造出数，第 3 章造出谈论「聚合」的语言，第 4、5 章把运算补全——整数定义为自然数的形式差（formal differences），有理数定义为整数的形式商（formal quotients），实数则经柯西序列的形式极限构造 (Tao, 2022)——不是戴德金截割。第 5 章五个小节的标题连起来就是一张施工单：柯西序列、等价的柯西序列、实数的构造、实数的序、最小上界性 (Tao, 2022)。而且每造出一层，都要先验证其基本性质再向上走：前言的叙述是，学生验证完整数的基本性质，才继续走到有理数；验证完有理数，再经柯西序列的形式极限走向实数 (Tao, 2022)。待到第 6 章序列的极限登场时，分析才真正开始；而那时，全部地基已逐层夯实。

这本书的取径，前言说得直白。实分析连同线性代数、抽象代数，是学生最早要「真正与严格证明的微妙之处较劲」的课程之一；于是这门课提供了「回到数学基础」（go back to the foundations of mathematics）的良机，得以对实数做一次「像样的、彻底的构造」；这促使作者「回到这门学科最初的起点，甚至回到自然数本身的定义」，把地基从头查验一遍 (Tao, 2022)。前言还立了一条方法论纪律——不循环论证（non-circularity）：「不用后来的、更高级的结果去证明早先的、更原始的结果」(Tao, 2022)。作为佐证，陶哲轩回忆当年的早期作业之一，是「只用皮亚诺公理」验证自然数加法的结合律，即练习 2.2.1 (Tao, 2022)。本章稍后就把这道作业原样做完。

在作者看来（此处的对比是本文的概括，非两书原文的自陈），这与 Rudin 一类经典分析教材的取径正好相反：后者多以实数系为预先给定的舞台，尽快进入点集结构与极限理论；《Analysis I》则把起点前移到自然数的定义，用将近半本书先把数系一件件造出来，再开始分析。陶哲轩自己对这本书的定位也是「互补」而非取代——2025 年发起 Lean 伴读的公告里，他回顾此书「有意与市面上许多优秀分析教材互补，更多聚焦于基础问题」（全文见下节）(Tao, 2025a)；互补的另一面正是差别：标准教材承接下来默认的东西，这本书从更深的起点重做一遍。代价是篇幅与耐心，收益是：书中没有一个数系是「大家都熟，从它做起」的——每个都从下一段构造中出生，连「显然」也要重新挣得；开课头几周，学生操练的不是不等式放缩，而是一砖一瓦的构造与验证。这一点恰是形式化的理想靶子：不预设任何数系的文本，翻译成 Lean 时无处可以藏匿直觉。

记号方面有一条须先交代：书中的后继记作 n++（而非逻辑教材常见的 S n），五条公理编号为 Axiom 2.1 至 2.5。往后读到 Lean 代码时请记住这个对应——仓库为贴合原书，给自建的自然数类型也定义了 ++ 后缀记号；而 Mathlib 一系的标准记法是 Nat.succ n。同一对象，两副面孔。

teorth/analysis：作者本人维护的伴读仓库

2025 年 5 月 31 日，陶哲轩在博客发布公告「A Lean companion to Analysis I」，同日建仓 teorth/analysis (Tao, 2025a)。公告先交代书的情况：「大约二十年前，我写了一本名为《Analysis I》的实分析教材。它有意与市面上许多优秀分析教材互补，更多聚焦于基础问题——自然数、整数、有理数与实数的构造——并提供足够的集合论与逻辑，让学生能在高度严格的水准上展开证明。」接着是动机：「因此我决定为《Analysis I》发起一个 Lean 伴读，把书中许多定义、定理与练习『翻译』成 Lean。特别地，这提供了做书中练习的另一条路：改填 Lean 代码里对应的那些 sorry。」(Tao, 2025a) 他还预期这份伴读「亦可兼作 Lean 与 Mathlib 的入门，兼作实分析的入门——颇有『自然数游戏』（Natural Number Game）的精神，后者与本书第 2 章实在有可观的主题重叠」，并从类型论一边给出理由：他构造标准数系时默认使用的那种「朴素类型论」，「与 Lean 的依值类型论吻合得很好——后者（除别的优点外）对商类型有一流的支持」(Tao, 2025a)。

仓库的形态（以下事实均出自笔者对快照 245b2e1，2026-09-04 的实读）：项目以 Apache 2.0 许可发布；README 自述为「Analysis I 的 Lean 形式化」，根模块 Analysis.lean 按书序导入全部章节文件；Analysis/ 目录下共 107 个 .lean 文件，采用扁平命名 Section_{章}_{节}.lean——第 2 章的皮亚诺公理在 Section_2_1.lean，加法在 Section_2_2.lean，乘法在 Section_2_3.lean。每个文件头部注明「Analysis I, Section X.Y: 标题」，并声明「All numbering refers to the original text」——定理与命题编号与书一致，这对逐条对照的读者是实打实的便利 (teorth/analysis, 2026)。覆盖面直到附录：数理逻辑基础（A.1–A.7）与十进制表示（B.1–B.2）各有对应文件；第 1 章导言则如后文引到的完成公告所言，因文体原因未形式化 (teorth/analysis, 2026)。工具链由 lean-toolchain 文件锁定在 leanprover/lean4:v4.29.0-rc8，Mathlib 以 git 依赖锁同一版本——第三章讲过，elan 会按这个文件自动选版，克隆仓库即得配套环境 (teorth/analysis, 2026)。书之外，仓库还在生长附加内容：测度论教材（Tao 的 Measure Theory）的形式化正在进行，另有物理单位制、有限概率与若干 Erdős 问题的解 (teorth/analysis, 2026)。

README 对翻译方针有明确自白：这份形式化「旨在成为对原文尽可能忠实的转述，同时展示 Lean 的特性与语法。特别地，它不为效率优化，某些地方可能偏离地道的 Lean 用法」；「书中定义、定理与证明的安排虽是教材的贴近转述，我不直接引用教材原文，而是适时给出对原书的指引。因此，这份形式化应被看作原著的注疏式伴读（annotated companion），而非替代品」(teorth/analysis, 2026)。两张姿态——忠实优先于地道，伴读而不僭越——决定了本章看到的一切代码的样子。

进度与协作同样有据可查。2025 年 7 月 15 日，陶哲轩在公告评论区宣布：「《Analysis I》现已完全形式化（导言一章除外——那一章文体严格程度低得多，关心的恰恰是那些不能翻译为形式证明的（不正确的）非正式论证）。」(Tao, 2025a) 贡献方面，按 GitHub contributors API（2026-09-14 访问）共 48 人；陶哲轩本人（teorth）以 1035 次提交居首，是绝对主力，其后 Chessing234（221 次）、aodecipher（195 次）、gaearon（101 次）等 (teorth/analysis, 2026)。发起人亲自写主体、社区补外围，与第四章介绍的 Mathlib 模式同构而规模更小。顺带一提，作者的个人书页如今写着：「本书没有官方解答手册。不过，有一个 Lean 伴读。」(Tao, 2026a)

五条公理与一个归纳定义

现在进入本章核心：皮亚诺公理的 Lean 实现。先摆出数学形态——书第 2.1 节的五条公理，沿用 n++ 记号 (Tao, 2022)：

  • 公理 2.1：0 是自然数。
  • 公理 2.2：若 n 是自然数，则 n++ 是自然数。
  • 公理 2.3：0 不是任何自然数的后继；即对任意自然数 n，n++ ≠ 0。
  • 公理 2.4：不同的自然数有不同的后继；即若 n++ = m++，则 n = m。
  • 公理 2.5（归纳原理）：设 P 为关于自然数的性质。若 P(0) 成立，且 P(n) 成立蕴涵 P(n++) 成立，则 P(n) 对一切自然数 n 成立。

在 Lean 里，这五条的落脚点是一个两行的归纳定义。以下及本章后文的 MyNat 代码，全部逐字取自笔者的本地验证文件（core Lean 4，Lean 4.33.1 编译通过，零错误、零占位证明，2026-09）：

lean
inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

第三章说过，每个归纳定义自动获得一个消去子。查证它：

lean
#check @MyNat.rec

本机输出，逐字照录（命令在 namespace MyNat 内运行，信息行显示的是命名空间内的短名 @rec）：

@rec : {motive : MyNat → Sort u_1} → motive zero → ((a : MyNat) → motive a → motive a.succ) → (t : MyNat) → motive t

第四章逐段读过 Nat.rec 的同款签名：一个动机、两份小前提（zero 情形与 succ 情形，后者内嵌归纳假设）、一个待消除的大前提。现在可以给出本章的核心论点：这五条公理被一个归纳定义整体吸收。逐条看吸收的方式，各不相同，而每一种都不需要 axiom 声明。

公理 2.1 与 2.2（0 是自然数；后继封闭）甚至不是定理，而是定义的语法事实。zero : MyNat 写在构造子清单里，公理 2.1 便已成立；succ : MyNat → MyNat 的类型就是「任何自然数的后继仍是自然数」，公理 2.2 便是这句话本身。数学公理在此化入类型的文法：要问「为什么 0 是自然数」，答案是——它被声明为这个类型的构造子。

公理 2.3 与 2.4 各值一行定理：

lean
theorem zero_ne_succ (n : MyNat) : zero ≠ succ n := fun h => nomatch h
theorem succ_inj {m n : MyNat} (h : succ m = succ n) : m = n := by injection h

证明短到近乎无物，因为内容仍在定义里。nomatch h 意为：假设 h : zero = succ n，则对 h 作模式匹配时无任何构造子组合可匹配——zero 与 succ n 出自两个不同的构造子，而归纳定义自带「构造子互不相交」与「构造子单射」的结构承诺（后者由 injection 策略使用：从 succ m = succ n 这类等式中「注射出」m = n）。一行证明不是省略，而是把公理的重量卸给了定义。

公理 2.5 的吸收最见本色：归纳原理就是消去子本身。MyNat.rec 的 succ 小前提内嵌归纳假设、动机落在 Prop 时整体即归纳法——第四章已演示 induction 生成的证明项恰是消去子的应用。第三章预告的那句话在此兑现：数学归纳法不是公理，而是构造的赠品。

五条公理，两条化为语法、两条一行定理、一条成为消去子——「公理」与「定理」的界碑在类型论里被挪了位置。检验这一论断有个干脆的办法：#print axioms。对上面这条从公理一路证到交换律的顶点做一次体检——

lean
#print axioms add_comm

本机输出，逐字照录：

'MyNat.add_comm' does not depend on any axioms

从五条「公理」出发推出的交换律，一条公理也不依赖。这不是文字游戏：书中作为推理起点的五条假设，在 Lean 里全部由「一个归纳定义加它的自动生成物」兑现，而这台生成机器的可靠性，就是第三章那段内核代码。

加法落地：定义方向决定证明形状

公理之后是运算。书第 2.2 节以 Definition 2.2.1 定义加法，递归在第二个参数上：任取自然数 n，规定 n + 0 = n；规定 n + (m++) = (n + m)++。MyNat 照书直译（结构递归的方程写法）：

lean
def add : MyNat → MyNat → MyNat
  | n, zero   => n
  | n, succ m => succ (add n m)

数值检验：2 + 2 = 4，rfl 一行——两边的 succ 嵌套按定义展开到同一形状（第四章「已完成的计算」），无须归纳：

lean
example : add (succ (succ zero)) (succ (succ zero))
        = succ (succ (succ (succ zero))) := rfl

对未知数成立的恒等式则必须归纳，而需要哪一条、不需要哪一条，完全由递归方向决定。在书的方向（对第二参数递归）下，add n zero = n 与 add n (succ m) = succ (add n m) 都是定义等式；反过来，0 + n = n 与 (succ m) + n = succ (m + n) 是「卡住的计算」，各需一次归纳：

lean
theorem zero_add (n : MyNat) : add zero n = n := by
  induction n with
  | zero => rfl
  | succ m ih => exact congrArg succ ih
 
theorem succ_add (m n : MyNat) : add (succ m) n = succ (add m n) := by
  induction n with
  | zero => rfl
  | succ k ih => exact congrArg succ ih

succ 分支里的 congrArg succ ih 是对等式两边同施一个函数的库定理：由 ih : add zero m = m 得 succ (add zero m) = succ m，而左端按定义就是 add zero (succ m)——归纳假设一步接力。有了这两块基石，前言里那道「只用皮亚诺公理验证加法结合律」的早期作业（练习 2.2.1）可以交卷了：

lean
theorem add_assoc (a b c : MyNat) : add (add a b) c = add a (add b c) := by
  induction c with
  | zero => rfl
  | succ k ih => exact congrArg succ ih

书中编号为 Proposition 2.2.4 的交换律：

lean
theorem add_comm (a b : MyNat) : add a b = add b a := by
  induction b with
  | zero => rw [zero_add]; rfl
  | succ k ih => rw [add, succ_add, ih]

zero 分支值得停一秒：rw [zero_add] 之后目标是 add a zero = a，rw 自带的收尾自反性在 reducible 透明度下打不开普通的 def，须补一个显式 rfl——第三章讲透明度时埋的细节，在此现身。succ 分支三步：先用 add 的定义等式把左端展开为 succ (add a k)，再用 succ_add 改写右端，最后 ih 接力。消去律（书中 Proposition 2.2.6）则演示「改写假设」：

lean
theorem add_left_cancel (a b c : MyNat) (h : add a b = add a c) : b = c := by
  induction a with
  | zero => rw [zero_add, zero_add] at h; exact h
  | succ k ih => rw [succ_add, succ_add] at h; exact ih (succ_inj h)

归纳时 Lean 自动把依赖目标的 h 一并还原重引入，每个分支里各得一条现成的假设；zero 分支两次改写后 h 已是 b = c，succ 分支改写后用公理 2.4 的定理形态 succ_inj 剥去后继、交给归纳假设。最后一条分辨自然数的两种来路——是零，或是某数的后继：

lean
theorem zero_or_succ (n : MyNat) : n = zero ∨ ∃ m : MyNat, n = succ m := by
  induction n with
  | zero => exact Or.inl rfl
  | succ k ih => exact Or.inr ⟨k, rfl⟩

这一条在书中通往正数与序的讨论；证明本身则再次是一行分支的归纳。

对照仓库：自证的第一层

MyNat 是笔者为教学复现的最小骨架；仓库的正文比它考究。Analysis/Section_2_1.lean 的做法是在 Chapter2 命名空间内自建一个自然数类型（全名 Chapter2.Nat，与 Mathlib 的 _root_.Nat 区分），声明与 MyNat 同形，多出一个派生子句 (teorth/analysis, 2026)：

lean
inductive Nat where
| zero : Nat
| succ : Nat → Nat
deriving Repr, DecidableEq  -- this allows `decide` to work on `Nat`

文件头注把路线交代得清楚：「书中自然数以纯公理方式处理，视其为一个服从皮亚诺公理的类型；这里我们则利用 Lean 原生的归纳类型，显式构造出一个服从这些公理的自然数版本。也可以走更公理化的路子——第 3 章对集合论正是那样做的：见本章尾声。」(teorth/analysis, 2026) 因为仓库里同时住着两种自然数，数字字面量常须写明类型以免歧义——下引代码里的 (4:Nat) 即是此意 (teorth/analysis, 2026)。五条公理随后逐一落地为定理与记号：

lean
instance Nat.instZero : Zero Nat := ⟨ zero ⟩
postfix:100 "++" => Nat.succ

公理 2.1 落为一个 Zero 类型类的实例（0 由构造子提供），公理 2.2 落为开篇交代过的 ++ 后缀记号——后继就是构造子本身。公理 2.3 与 2.4 同样落为短定理（by_contra 先取反证假设），文档串各注明库中对应的定理作对照，但证明不依赖它们：

lean
theorem Nat.succ_ne (n:Nat) : n++ ≠ 0 := by
  by_contra h
  injection h
lean
theorem Nat.succ_cancel {n m:Nat} (hnm: n++ = m++) : n = m := by
  injection hnm

公理 2.5 落为一条定理，用内建 induction 策略证明——而内建策略的底层，正是归纳定义自动生成的消去子：

lean
theorem Nat.induction (P : Nat → Prop) (hbase : P 0) (hind : ∀ n, P n → P (n++)) :
    ∀ n, P n := by
  intro n
  induction n with
  | zero => exact hbase
  | succ n ih => exact hind _ ih

此后全书引用的「归纳原理」就是这条定理。后文证明里反复出现的 revert n; apply induction，施加的正是它——先把变量放回目标，再调用自证的公理 2.5。书中「由归纳原理」五个字，在仓库里有了逐字对应的名词。

五公理之后，书 2.1 节的第一批命题仓库也照单全收。Proposition 2.1.6（4 ≠ 0）：

lean
theorem Nat.four_ne : (4:Nat) ≠ 0 := by
  -- By definition, 4 = 3++.
  change 3++ ≠ 0
  -- By axiom 2.3, 3++ is not zero.
  exact succ_ne _

change 把目标改写成定义等价的形式——先把 4 还原成 3++，再调用公理 2.3 的定理形态收尾。Proposition 2.1.8（6 ≠ 2）则给了两版：一版按书走，反证后两次 succ_cancel 手工剥去后继，归结到 4 ≠ 0 矛盾；另一版一行了账：

lean
theorem Nat.six_ne_two' : (6:Nat) ≠ 2 := by
  decide

decide 对可判定命题直接按定义求值，声明处的派生子句正是为它铺路——代码注释原话："this allows decide to work on Nat" (teorth/analysis, 2026)。两版对照是「书证法与机器证法」的缩影：前者复现推理链，每步可与人读；后者一步算出答案，推理链收进机器。而两版最终都经同一内核检查，可靠性并无差别。

加法一节暴露出一个有趣的技术抉择。书 Definition 2.2.1 对第二参数递归，仓库偏偏反过来，对第一个参数递归 (teorth/analysis, 2026)：

lean
abbrev Nat.add (n m : Nat) : Nat := Nat.recurse (fun _ sum ↦ sum++) m n

Nat.recurse 是第 2.1 节按书中 Proposition 2.1.16（递归定义定理）自建的递归算子：给定步进函数与基值，对第一个变元 n 递归——基值取 m，每步对累计值施一次后继。它的两条计算方程各由 rfl 成立：

lean
theorem Nat.recurse_zero (f: Nat → Nat → Nat) (c: Nat) : Nat.recurse f c 0 = c := by rfl
theorem Nat.recurse_succ (f: Nat → Nat → Nat) (c: Nat) (n: Nat) :
    recurse f c (n++) = f n (recurse f c n) := by rfl

第 2.1 节并为这台算子证了唯一性——满足这两条方程的函数存在且只有一个 (teorth/analysis, 2026)；加法就架在它上面。方向一换，哪些恒等式免费、哪些要付归纳的代价，就整个对调了。仓库里 (n++) + m = (n+m)++（Nat.succ_add）按定义 by rfl 直接成立；而 n + (m++) = (n+m)++（Nat.add_succ，书 Lemma 2.2.3）需要一次归纳：

lean
lemma Nat.add_succ (n m:Nat) : n + (m++) = (n + m)++ := by
  -- this proof is written to follow the structure of the original text.
  revert n; apply induction
  . rw [zero_add, zero_add]
  intro n ih
  rw [succ_add, ih]
  rw [succ_add]

同一枚硬币在 MyNat 里翻了面：add n (succ m) = succ (add n m)（add_succ 型）在仓库要付归纳，在书的方向下免费；succ_add 在仓库免费，在书的方向下要付归纳。何者 rfl、何者归纳，正好互换——这不是哪一边写错了，而是递归定义的固有不对称：定义只能选一个方向递归，另一方向的恒等式就得靠归纳补回来。书中 2.2 节的论证结构（先证 n + 0 = n，再证另一侧，最后合成交换律）正是这种不对称的展开。

仓库对书结构的忠实一直延伸到证明体。书中 Lemma 2.2.2（n + 0 = n）的仓库证明：

lean
/-- Lemma 2.2.2 ({lean}`n + 0 = n`). Compare with Mathlib's {name}`Nat.add_zero`. -/
@[simp]
lemma Nat.add_zero (n:Nat) : n + 0 = n := by
  -- This proof is written to follow the structure of the original text.
  revert n; apply induction
  . exact zero_add 0
  intro n ih
  calc
    (n++) + 0 = (n + 0)++ := by rfl
    _ = n++ := by rw [ih]

calc 链的两步，对应书里「先由定义展开、再用归纳假设」的手算。Proposition 2.2.4（交换律）同样照书走：

lean
theorem Nat.add_comm (n m:Nat) : n + m = m + n := by
  -- this proof is written to follow the structure of the original text.
  revert n; apply induction
  . rw [zero_add, add_zero]
  intro n ih
  rw [succ_add]
  rw [add_succ, ih]

与 MyNat 版对照着读颇有意味：同为交换律，两边的 zero 分支都要同时用到两侧的零恒等式（仓库 rw [zero_add, add_zero]，MyNat rw [zero_add] 后显式 rfl——后者因 add n zero 恰是定义等式）；succ 分支则各自先动用己方免费的那条（仓库用 succ_add，MyNat 展开 add），再补对方付费的那条（仓库 add_succ，MyNat succ_add）。同一道题的两个解，像镜像一样对称——递归方向的抉择，从定义一路传导到最后一行证明。

消去律可以把这面镜子再照一次。仓库 Proposition 2.2.6 的证明：

lean
/-- Proposition 2.2.6 (Cancellation law).
    Compare with Mathlib's {name}`Nat.add_left_cancel`. -/
theorem Nat.add_left_cancel (a b c:Nat) (habc: a + b = a + c) : b = c := by
  -- This proof is written to follow the structure of the original text.
  revert a; apply induction
  . intro hbc
    rwa [zero_add, zero_add] at hbc
  intro a ih hbc
  rw [succ_add, succ_add] at hbc
  replace hbc := succ_cancel hbc
  exact ih hbc

三步与 MyNat 版逐一对应：先把假设改写到能用——zero 分支两次 zero_add、succ 分支两次 succ_add，与 MyNat 的 rw [zero_add, zero_add] at h、rw [succ_add, succ_add] at h 连改写的次数与位置都一致；再剥后继——仓库用公理 2.4 的定理形态 succ_cancel，MyNat 用同一公理的 succ_inj；最后交给归纳假设。两处小差别也值得看：仓库版 revert a 把假设一并还原，故每个分支要 intro 重新引入，MyNat 版由 induction 策略自动还原重引入（本章加法一节已见过这层机制）；仓库惯用的 rwa 在改写之余直接以所得假设闭合目标，replace 则就地替换一条假设。骨架相同，皮肉随方言——README 承诺的「忠实优先于地道」，在两份证明的并排对照里可以逐行指着读。

对照仓库：公理化的第二层

第 2 章的尾声（Analysis/Section_2_epilogue.lean）把戏演足。前半是交接仪式：定义一个双向转换函数，证明它是双射，且保持加法、乘法、序与乘幂——Chapter2.Nat 与 Mathlib 的 ℕ 在诸种意义下同构，此后全书改用后者 (teorth/analysis, 2026)。后半是本节的主角。文件头注自陈：「本节后半将给出自然数的一个完全公理化的处理。前三节的处理只是部分公理化，因为我们用了自然数的一个具体构造 Chapter2.Nat——一个归纳类型——并用该归纳类型构造出递归子。这里我们给出一些练习，展示如何直接从皮亚诺公理完成同样的任务，而无需知道自然数的具体实现。」(teorth/analysis, 2026) 于是五条公理以它们在书中的本来面目回归——打包为一个结构体的五个字段：

lean
/-- The Peano axioms for an abstract type {name}`Nat` -/
@[ext]
structure PeanoAxioms where
  Nat : Type
  zero : Nat -- Axiom 2.1
  succ : Nat → Nat -- Axiom 2.2
  succ_ne : ∀ n : Nat, succ n ≠ zero -- Axiom 2.3
  succ_cancel : ∀ {n m : Nat}, succ n = succ m → n = m -- Axiom 2.4
  induction : ∀ (P : Nat → Prop),
    P zero → (∀ n : Nat, P n → P (succ n)) → ∀ n : Nat, P n -- Axiom 2.5

随后给出两个实例。Chapter2_Nat 用第 2.1 节自证的定理逐字段填充；Mathlib_Nat 转而引用 Mathlib：

lean
/-- The Mathlib natural numbers obey the Peano axioms. -/
def Mathlib_Nat : PeanoAxioms where
  Nat := ℕ
  zero := 0
  succ := Nat.succ
  succ_ne := Nat.succ_ne_zero
  succ_cancel := Nat.succ_inj.mp
  induction _ := Nat.rec

最后一行值得多看一眼：为 Mathlib 的自然数填写「公理 2.5」字段的，正是 Nat.rec——那个由归纳定义自动生成的消去子。公理化的包装之下，填进去的仍是构造的赠品。

这层抽象买到了什么？在作者看来有三样。其一，可替换性：PeanoAxioms 是「一个类型加五条性质」的记录，任何填得满五个字段的类型都算数——正文自证的 Chapter2.Nat 与 Mathlib 的 ℕ 并列为实例，两种自然数经由尾声的同构交接，此后各章换用 ℕ 而理论不断档。其二，可教性：尾声的练习要求不依赖任何具体实现、只从这五个字段出发重建递归与归纳——做练习的人被迫分辨，哪些定理真的只需要皮亚诺公理，哪些偷偷用了构造的细节。其三，一个数学论断的落点：满足这组公理的结构在等价意义下唯一——公理确实「刻画」了自然数；这条唯一性在仓库里被安排为留白的练习（下节再谈）。README 对这套安排的说明是：「例如，第 2 章不依赖 Mathlib、独立发展一套自然数理论，但后续所有章节都改用 Mathlib 的自然数。（第 2 章的尾声证明两种自然数概念同构。）」(teorth/analysis, 2026)

在作者看来，这个双层结构本身是「公理与构造之辨」的活教材：正文一层，把书中的公理逐条证明为定理——公理的地位被构造吸收；尾声一层，把公理重新升格为抽象结构的假设字段，再证明两种现成的自然数（自建的与 Mathlib 的）都是它的实例——公理的地位又被抽象还原。两层合观，回答了一个初学者的典型困惑：「Lean 里的皮亚诺公理在哪？」——它们既不在公理声明里（被构造吸收），也没有消失（可作为结构字段随时恢复）；形式系统允许两种呈现，并让它们互相印证。

三件套学法：教材、源码、练习

案例看完，说说怎么用它学。这本教材配这座仓库，恰好构成「教材 + 源码 + 环境」的三件套，学与练都在一条动线上。

第一件是读书。README 的定位说得很清楚：这是「注疏式伴读而非替代品」，仓库不直接引用教材原文，只给出指引 (teorth/analysis, 2026)——编号是两者之间的桥。第二件是读源码。每章读完，打开对应的 Section_{章}_{节}.lean：文件头注明章节与标题，声明「All numbering refers to the original text」(teorth/analysis, 2026)，书中每条 Proposition 2.2.4、Lemma 2.2.2 都能按号索骥。读的时候带着本章的两把钥匙：其一，仓库证明里 revert …; apply induction 调用的是自证的公理 2.5 定理，读作书中「由归纳原理」；其二，加法恒等式哪条免费、哪条付费，先看 Nat.add 的递归方向再判断。第三件是做练习，而练习的形态已在开头的公告引文里露过面：书中留给读者的练习，在仓库里渲染为 sorry (teorth/analysis, 2026)。sorry 是 Lean 认可的占位证明——编译器接受它，但会告警。仓库以编译选项 -Dwarn.sorry=false 关掉这族警告（配置注释写着 "remove when project is complete"，工程仍在推进的自况）(teorth/analysis, 2026)。对学习者，这个机制刚好反过来用：fork 仓库，按 README 的邀请「试手这些练习」(teorth/analysis, 2026)，找到编号对应的 sorry，换成自己的证明，编译通过练习即告完成——批改是编译器做的，不需要解答手册（本来也没有，作者明说不打算把解答放进仓库）(teorth/analysis, 2026)。

第 2 章的练习尤其适合作起点。除了前言点名的结合律（2.2.1），这一组还包括唯一前驱、序的基本性质、三歧性、强归纳与倒退归纳，以及乘法的对应命题，共十二处练习标注；尾声的练习则要求脱离具体构造、直接从 PeanoAxioms 出发重建理论——其中最见野心的一组是证明任意两个服从皮亚诺公理的结构彼此等价、且这样的等价唯一：皮亚诺公理刻画的对象「只有一个」，这条数学事实在仓库里就是留白待填的 sorry (teorth/analysis, 2026)。陶哲轩自己判断这条路线对入门友好：伴读「亦可兼作 Lean 与 Mathlib 的入门」，与「自然数游戏」精神相通、主题重叠可观 (Tao, 2025a)。环境搭建不劳此刻分心——elan 按 lean-toolchain 自动配好版本，安装步骤第八章统一交代。至于这项事业的下一步，他已有打算：2025 年 9 月 29 日评论道，「我正在教 245A（测度论），同时开始把教材形式化……我希望让班上一些学生参与进来，或许也借机测试一些较新的自动形式化工具」(Tao, 2025a)。让机器来填 sorry——这个念头正是下一章的主题。

皮亚诺公理的故事讲完了，收在一处对照上：《数学原理》为给「1+1=2」这样的平凡事实以无懈可击的根据，铺设了庞大得惊人的符号机器（第一章）；而在这座 2025 年动工的仓库里，五条公理化作两行定义、两行定理与一个自动生成的消去子，交换律的证明经 #print axioms 体检，一条公理也不依赖。同一门生意，两种账法。机器读证明读到公理这一层，读到的已经是自己写下的定义。

六、AI 与形式化的交汇

第五章结尾，陶哲轩说他想把「较新的自动形式化工具」交给学生测试。让机器来填 sorry——这个念头并非他一人独有，而是近三年形式化社区与人工智能社区共同的话题。第一章归纳形式化的四重价值时，第四条是「人工智能的基础设施」：机器可检查的数学文本，同时是可以供机器检索与学习的环境。本章兑现这个承诺，也兑现它的限度。

训练场与基准：LeanDojo 与 miniF2F

先看环境一侧为什么重要。训练一个会写证明的模型，最大的瓶颈往往不是模型，而是判卷：自然语言的数学证明没有廉价的对错信号，人工标注既贵又慢。Lean 恰好自带判卷者——第三章讲过的内核。一个生成的证明项，要么通过类型检查，要么不通过，reward 信号即时、客观、可无限重复；Mathlib 的 28.7 万条定理（截至 2026-09，第二章已引）则提供现成的语料与课程表。

把这个环境整理成研究基础设施的代表性工作，一是 LeanDojo：开源的 Lean 证明场地、数据集与基准，2023 年发表于 NeurIPS 的数据与基准轨道（口头报告）(Yang et al., 2023)。它的一个特色是前提标注（premise annotation）：把 Mathlib 每条定理的证明所引用的前提逐条标出，于是「该用哪条已有引理」从写作直觉变成一个可学习的检索问题，论文附带的 ReProver 模型正是检索增强的证明器 (Yang et al., 2023)。二是 miniF2F：副标题即「跨系统的奥赛级形式数学基准」（a cross-system benchmark for formal Olympiad-level mathematics），共 488 题，划分为 244 题验证集与 244 题测试集，同一批题目在 Lean、Metamath、Isabelle 三个系统中各有一份形式化，题目取自 AIME、AMC、IMO 及高中与本科课程 (Zheng, Han & Polu, 2022)。跨系统的设计让「模型的能力」与「系统的差异」可以分开度量。这两个名字此后反复出现在 AI 定理证明的论文里——它们是这条研究线的公用场地。

AlphaProof：形式化路线的代表作

2024 年 7 月 25 日，Google DeepMind 发布官方博客：AlphaProof 与 AlphaGeometry 2 两套系统联手，解出当年国际数学奥林匹克（IMO）六题中的四题，得 28/42 分——「首次达到与银牌得主同等的水平」，且解出的每题皆为满分；当年金牌线为 29 分，正式参赛的 609 名选手中 58 人达金牌 (Google DeepMind, 2024)。

技术路线以官方博客为准。AlphaProof「是一个在 Lean 形式语言中训练自己证明数学命题的系统」，它把一个预训练语言模型与 AlphaZero 强化学习算法耦合——后者曾自学掌握国际象棋、将棋与围棋 (Google DeepMind, 2024)。自然语言一侧的入口也是模型：他们「微调了一个 Gemini 模型，把自然语言题面自动翻译为形式语句」(Google DeepMind, 2024)。需要如实补记的是：在 IMO 2024 的这次运行中，六道题的题面仍由专家在赛前人工译为形式语言；两道组合题始终未解；单题耗时从数分钟到三天不等 (Google DeepMind, 2024)。分工上，AlphaProof 解出两道代数题与一道数论题——其中包括全场最难的第六题，正式比赛中仅五名人类选手解出；AlphaGeometry 2 解出几何第四题，形式化之后 19 秒完成 (Google DeepMind, 2024)。作为参照，AlphaGeometry 2 在赛前基准上可解过去二十五年间 83% 的 IMO 几何真题，前代为 53%（前代成果刊于 Nature）(Google DeepMind, 2024; Trinh et al., 2024)。方法论细节后来整理为 Nature 论文 (Hubert et al., 2025)。

在作者看来（以下解读为本文立场），形式化在这条路线里扮演的角色需要说准：它不是输出给人阅读的证明格式，而是训练与搜索的护栏。强化学习需要奖励信号，内核即时给分；证明搜索的每一步都可判定，错了立刻知道。代价是把「AI 自己读题」这一环暂时让渡了出去——题面靠人译，正说明自然语言理解与形式推理当时尚未接通。

一年之后：另一条路线拿了金牌

2025 年 7 月 21 日，同一机构的官方博客宣布：进阶版 Gemini Deep Think 六题解出五题且皆为满分，得 35/42，「达到金牌水平」(Luong & Lockhart, 2025)。官方特意给出与上一年的对比，原话值得整段移录：在 IMO 2024，AlphaGeometry 与 AlphaProof「需要专家先把题目从自然语言翻译成 Lean 一类领域特定语言，证明也要反向译出，且需要两到三天的计算。今年，我们的进阶 Gemini 模型以自然语言端到端运行，直接从官方题面产生严格的数学证明——全部在 4.5 小时的比赛时限之内」(Luong & Lockhart, 2025)。

两条路线的关系，在作者看来不是取代而是分岔。自然语言端到端贴近「AI 如同人类选手参赛」的叙事；形式化路线放弃这个叙事，换来可验证性。对奥林匹克这种有标准答案的考试，端到端的胜利当然重要；而数学研究没有标准答案在场——一个研究命题的对错，恰恰就是要在证明写完之后才能判定。在那里，未经内核检查的输出无论多流畅，都还停留在「提案」的地位。这也是为什么陶哲轩在设想研究场景时，把「严格的 Lean 翻译」列为「用于研究品质发表前的必要条件」（见下节）。

陶哲轩的实验与账目

陶哲轩是这条交汇线上最持续的高产观察者，他的论述有清楚的时间层次。2023 年 4 月，他给人机分工记过一笔四档账（以下概述所据为原帖，Mastodon，2023-04-23）：日常熟练任务，AI 无增益；有专长而缺练习的任务，AI 可代拟初稿，自己验证润色；无专长而不要求高可靠的任务，可把 AI 当顺手的搜索引擎；无专长且要求高可靠的任务，AI 与自己都不可恃，须问人类专家 (Tao, 2023c)。这份账目的价值在于它的不对称：增益出现在「有专长缺练习」与「无专长低风险」两档——AI 放大的是已有的判断力，而不是替代它。

2026 年 4 月，他把数学研究的问题求解粗分为三个组件：证明的生成（找到解法）、验证（核对解法成立）、消化（digestion——「理解解答的本质，置于既有文献的脉络中，有效地总结与讲述它，并获得对其它相关问题的洞见」）(Tao, 2026b)。这个分解对本文的主题是一把量尺：机器近年的全部进展集中在生成与验证两端，而「消化」几乎原封不动地留给了人。

他自己的实验对应地嵌在这些档位里。2024 年 6 月，他向 ChatGPT 口述一个幂级数问题的证明梗概，模型产出了全文——他的自评是：「在我看来 GPT 表现相当好，把我的梗概扩写成连贯而相当严格的完整证明。但这不是我在那篇访谈里设想的全部——特别是，为保证正确性所需的严格 Lean 翻译还缺失，而我认为那是这套工作流能用于研究品质发表之前的必要条件」(Tao, 2024b)。那段访谈里的设想要激进得多：「将来，我们不再亲手把证明写成文稿，而是向某个 GPT 讲解；GPT 边听边试着把它形式化为 Lean。如果一切通过，GPT 会（基本上）说：这是你论文的 LaTeX 版，这是你论文的 Lean 证明。你愿意的话，我可以按这个键替你投给期刊」(Drösser, 2024)。对照之下，2023 年 12 月他给出的近期预期务实得多：AI 现实的目标，是自动填上他当日示例中那种「原子级 sorry」的可观比例，让蓝图更快变成正式的 Lean 证明 (Tao, 2023a)。从愿景、实验到预期，三段引文放在一起，落差与方向都写在明处。

还有一类实验干脆把「机器生成、机器验证」做成交互的协作范式。2024 年 9 月，陶哲轩发起泛代数试点项目 Equational Theories：magma 上至多含四个运算符号的等式律共 4,694 条，两两之间的蕴涵共 4,694×4,693 = 22,028,942 条待证或反驳，由社区以人机协作方式在 Lean 中推进 (Tao, 2024a)。他自陈此中深意：传统上数学研究项目由一至五位专家组成，人人熟悉全部细节方能互审；而这种范式——用他的原话——「也可用于探索新的数学，而不只是形式化已有的数学」(Tao, 2024a)。

自动形式化：愿景与落差

把自然语言的数学翻译成形式语言，这个方向叫自动形式化（autoformalization）。愿景已经见过（向 GPT 讲证明、它边听边译）；现状的落差有三层（以下为作者对所引文献的综合）。

其一，正确性缺口。模型产出的文本可以句句通顺而整体不成立——未经内核检查之前，「像证明」与「是证明」没有便宜的分界。陶哲轩 2024 年实验的自评即是一手例证：扩写成功的 LaTeX 全文，距离可担保的 Lean 翻译仍隔着一道必要的关卡 (Tao, 2024b)。他更早的说法把这类输出定位为「答案的初始近似，随后以更传统的方法加以精化」(Tao, 2023b)。

其二，前提失配。库里的引理以十万计，写出下一步之前先要「知道该用哪一条」；名称对不上、签名记错、上下文缺省——这些在自然语言里靠读者的默会知识兜底的事，在形式语言里全部变成显式缺口。LeanDojo 把前提做成标注数据、把证明变成检索问题，正是对这一层的正面回应 (Yang et al., 2023)。

其三，工程路线的迂回。既然一步到位的翻译不可靠，研究转向两段式：Draft, Sketch, and Prove 让模型先把非形式证明转写为形式「草图」，再由自动证明器补全细节（实验在 Isabelle 上完成，非 Lean）(Jiang et al., 2023)；Baldur 则干脆让大模型生成整个证明，并为「生成后不通过检查」的情形配备自动修复（同样以 Isabelle 为对象）(First et al., 2023)。修复环节的存在本身，就是首发命中率不高的自供状。

落差如此，方向也如此。第五章那座仓库之所以可行，靠的是「编号对照原书」的人工锚点；第六章这些工作想做的，是把锚点也交给机器。锚点交出去之日，第一章说的那条闭环——机器生成、机器验证、人提问并把关——才算真正合拢。

七、限度与批评

前面六章都在讲这项事业能做什么；本章清点它的账单。第一章欠下两笔债——人力与时间的细账、「绝对可靠」的边界——此处一并偿还。形式化不是免费午餐：它用一种可度量的成本，换一种可审计的可靠性；把成本与边界如实摆出，比任何颂歌都更利于判断它的位置。

膨胀的账：de Bruijn 因子

形式化文本比原数学文本长多少？这个比值有个名字：de Bruijn 因子——得名于第一章那位德布鲁因，他观察到这个比值在一份形式化内部大致恒定。经典测出自 Wiedijk 2000 年的技术笔记：对一份 Mizar 体系的样例文本，非形式原文 7.7K 字节，形式化后 35.3K，表观因子 4.6；两边各自压缩后为 2.6K 对 8.0K，内在因子 3.1 (Wiedijk, 2000)。文献给出的锚点跨度颇大：Mizar 体系常引的区间约 3–5（Wiedijk 此例即落在其中）；德布鲁因本人对 Automath 的估计约 20（Ayers 的博士论文导言转述）(Ayers, 2019)；陶哲轩 2025 年在《美国数学会通讯》给出的估计亦约 20——但须注意他的口径已从「长度之比」换成「难度之比」，原话是：「写出一个正确形式证明与写出一个正确非形式证明的难度之比，目前仍远高于一（我估计约 20），但在下降。我认为不存在把它压到一以下的根本障碍，尤其是与 AI、SMT 求解器等工具的整合加深之后——那将是变革性的」(Tao, 2025b)。引用这些数字的诚实做法，是同时注明口径与年代：de Bruijn 因子不是物理常数，它随工具、库与社区熟练度的变化而漂移，而近年的漂移方向向下。

时间的账

第一章的四个里程碑，此处补上时长刻度。四色定理的形式化复核距原证明二十九年；开普勒猜想自 1998 年宣布，Flyspeck 项目 2014 年完成，其中形式化本体约二十个工作人年（第一章已引）；奇数阶定理十五人协作逾六年；液体张量实验自 2020 年 12 月挑战帖起，2021 年 5 月 28 日验完朔尔策自认最没把握的部分，2022 年 7 月 14 日全部完成，前后约十九个月 (Scholze, 2020; Scholze, 2021; Mathlib 社区, 2022)。

同一本账上也有近年才出现的低刻度。陶哲轩记录：PFR 猜想的证明「人类写就的版本长 33 页、大体自足，约二十名协作者在三周内完成了形式化」(Tao, 2025b)。三周对二十人年——两个数字的差距，度量的是库的成熟、工具链的顺畅与熟练者的数量，而非定理本身的难易。反过来的大刻度同样有据：Buzzard 已宣布费马大定理的形式化项目，他估计至少需要五年 (Tao, 2025b)。在作者看来，成本结构里最难压缩的一项是人才：同时懂数学内容与 Lean 工程的人，全球不过数百人量级（Mathlib 的三百余提交作者、第五章仓库的 48 位贡献者，即是这个池子的实测口径）。工具可以下载，熟练不能。

验证不等于理解

机器验证的是「每一步推理合法」，不是「这个证明被人理解」。陶哲轩的三组件分解在这里恰好可用：机器的进展集中在生成与验证，而第三组件——消化，理解解答的本质、置于文献脉络、有效讲述并获得迁移的洞见 (Tao, 2026b)——不因内核通过而自动解决。

数学哲学里久有「解释性证明」（explanatory proof）与「仅仅令人信服的证明」之辨（以下讨论为作者立场的申说，非文献转述）。形式证明天然落在后一端：它把「为什么行得通」压平为「凭什么成立」，一个经检查的证明可能仍不告诉任何人它为何该如此构造。形式化还会改写证明的形状——第五章那组镜像证明即是缩影：同一个交换律，递归方向一换，免费的恒等式与付费的归纳整个对调，口算带过的对称性变成显式的改写序列。更大的尺度上，一部书的形式化会把叙述主线重组为引理网络。得的一面，每一步的依据显式化，结构依赖一望可知；失的一面，阅读的线性叙事被打散——「读证明」有变成「查证明」的危险。朔尔策在液体张量实验里的自评提供了一个注脚：半年总结时，他对主证明宣布「再无剩余疑虑」，同时自评实验「大概完成了一半」——所指是形式化整体尚余一半未完成，当时验完的只是他本人没有把握的那部分论证，全部完成要到次年 7 月 (Scholze, 2021)。验证给出的是确信；确信之外，工作与理解都仍须另挣。

信任的边界

第一章许诺过「绝对可靠的边界」，第三章已经给了一半答案，此处补全为四条。

其一，小内核不等于零风险。第三章引过的 2026 年 8 月内核缺陷（PR #14807）表明，数百行至数千行的内核同样会出错，且错误真实到可以推出 False (de Moura, 2026)。其二，防线的真正构成：缺陷会被发现、公开、修复——同批另有 #14806、#14843 两处挂 soundness 标签的相关修复；而独立实现的交叉验证在关键时刻显出价值，该伪证骗过了另一个实现 nanoda，作者却「相信 lean4lean 外部内核没有这个缺陷」(de Moura, 2026)。可靠性在这里是一种运维性质，靠公开与冗余维持，而非一次性担保。

其三与其四，则是两条系统性的边界。其三，陈述失配（此为作者论证）：机器保证的是「这个形式命题的证明无一步漏检」，并不自动保证「这个形式命题就是你心里那个定理」。翻译的忠实性落在系统之外——第五章的仓库用「编号与原书一致」来锚定它，第三章的 #print axioms 把全部假设登记在案；手段存在且有效，但最后一寸始终要人走。其四，哥德尔限度的工程化表述（呼应第一章）：不完全性定理禁止的是「系统自证一致性」的宏大纲领；工程实践从不试图自证，而是把信任压缩到可审计的最小集合——内核、公理清单、翻译——并接受这个集合自身的正确性靠经验、公开与交叉验证维持。这是一门可靠性工程，不是一份元数学的保证书；它的力量与它的谦逊是同一件事。

四条边界摆完，结论仍然是：在「具体证明的每一步都受过检查」这个意义上，形式化的可靠性没有任何人类制度可以比拟——开普勒猜想十二人审稿小组产出的「确信」（见引言），正是它所要超越的东西。边界划清之后，这份可靠性才谈得上被正确地信任。

八、学习路径与资源

第四、五章多次把安装与入口推到本章，现在兑现。以下资源全部经笔者于 2026 年 9 月逐条访问验证，中文资源尤以实测为限、宁缺毋滥。

装环境

官方推荐路径就一条：VS Code 加官方 Lean 4 扩展，「扩展会引导完成其余安装」，包括版本管理器 elan (Lean 官网, 2026)。Windows 用户若走命令行，elan 仓库 README 给出的官方命令（要求 PowerShell 7.4.1 以上）是两步：先 curl -O --location https://elan.lean-lang.org/elan-init.ps1 下载安装脚本，再 powershell -ExecutionPolicy Bypass -f elan-init.ps1 执行 (leanprover, 2026)。elan 的职责第三章已经见过：读 lean-toolchain 文件，自动选版下载——克隆一个带该文件的仓库（如第五章的 teorth/analysis），环境即自动配齐。本机实况（Windows 11，2026-09 实测）：elan 默认解析 stable 工具链至 Lean 4.33.1、Lake 5.0.0，即本文第四、五章全部示例所用的环境；未遇平台性障碍。新项目用 lake init 生成骨架（第三章的最小项目即由此而来），构建与缓存的行为第三章已述。不想安装的读者，官方另有在线编辑器 Lean Web（live.lean-lang.org），浏览器即开即用 (Lean web editor, 2026)；下面第一站的游戏本身也全程在浏览器里。

进阶路线

第 0 站，自然数游戏（Natural Number Game，NNG4）：关卡制教学游戏，托管于 Lean 游戏服务器（adam.math.hhu.de），从「0 是自然数」一路打到归纳，全程无需安装 (Buzzard & Eugster, 2026)。官方仓库含完整中文翻译，游戏内可切换语言。陶哲轩自己把它当作《Analysis I》伴读的精神同类 (Tao, 2025a)。

第 1 站，《Theorem Proving in Lean 4》（TPiL4）：本文第三、四章反复引用的官方教程，概念与机制的总纲 (Avigad et al., 2026)。第 2 站，《Mathematics in Lean》：面向数学工作者，以 Mathlib 为环境，教法就是第四章说的「读签名、组装证明」(Avigad & Massot, 2026)。两条支线按口味取用：偏重证明写作训练的，有 Heather Macbeth 的《The Mechanics of Proof》，一部用 Lean 教严格证明的分析预备教材 (Macbeth, 2026)；偏重语言与编程的，有《Functional Programming in Lean》(Christiansen, 2026)。第 3 站，Mathlib 本体：doc-gen4 生成的文档站、成文的命名约定、以及直接读源码 (leanprover-community, 2026)；遇到问题时，社区中枢在 Zulip（leanprover.zulipchat.com），各水平的提问都受欢迎 (Lean 社区, 2026)。第 4 站，回到第五章的 teorth/analysis (teorth/analysis, 2026)。

用《Analysis I》配 Lean 的具体学法，第五章的三件套已有纲领，这里补操作细节。先读书：仓库是「注疏式伴读而非替代品」，编号是书与码之间的桥 (teorth/analysis, 2026)。再对照：每读完一小节，打开对应的 Section_{章}_{节}.lean，带着那两把钥匙——revert …; apply induction 读作书中「由归纳原理」，恒等式哪条免费先看 Nat.add 的递归方向。最后动手：fork 仓库，按编号找 sorry，换成自己的证明，编译通过即完成——批改是编译器做的。给两类读者各有一句建言：只想学分析的，把仓库当一部自动批改的习题集，证明写不过去时回书里找思路，正是「不循环论证」的训练；想学 Lean 的，从第 2 章的皮亚诺公理入手，它比 NNG 略深而主题重叠 (Tao, 2025a)。

关于节奏与心态，附一段作者建言（非文献转述）。第一，把「报错」当正常态：Lean 的错误信息指明位置与原因，第四章说的目标视图让每一步都可观察——学习曲线陡的部分不在数学，而在与编辑器的磨合，一两周可过。第二，养成「先查后证」的反射：动笔前先 #check、exact?、Loogle 一轮，第四章引过的教训是查库常比自证便宜。第三，卡住时去 Zulip，README 明言各水平提问都受欢迎 (leanprover-community, 2026)——把问题连同最小示例贴出去，通常当日有答。第四，别追求「地道」：第五章的仓库宁可偏离惯用法也要贴合原书，教学如此，起步亦然；写得出、编得过、读得懂自己的证明，风格可以后来再学。

中文资源

中文资源目前仍少，此处只列实测可访问者。Lean 中文文档（leanprover.cn）由 Lean-zh 社区维护，含主页、交互工具、项目教程与 Mathlib4 帮助，已译介《定理证明》《形式化数学》《函数式编程》《元编程》等材料 (Lean-zh 社区, 2026)；TPiL4 的中文翻译有两处镜像，一在该社区站内，一在译者 subfish-zhou 的独立站 (Lean-zh 社区, 2026; subfish-zhou, 2026)；自然数游戏的中文界面如前述在官方仓库内 (Buzzard & Eugster, 2026)。其余散见的中文教程品质与维护性参差，本文不具名推荐。

结语

引言从一场审稿马拉松讲起：十二位专家数年的工作，产出的仍然是「确信」而不是「认证」。近三十年后回看，那场马拉松的意义或许在于它把问题问清楚了：当证明的规模超过任何审阅者的耐心，数学界需要一种新的文本。本文记下的，就是这种文本如何从《数学原理》的手工符号机器，经 Automath、Coq、Isabelle 一路走到 Lean 与 Mathlib，又在《Analysis I》的伴读仓库里落到一部具体教材的每一道练习。

这种文本正在获得软件的全部属性。它可版本化——第五章的仓库以 git 管理，1,035 次提交铺出一条完整的施工史；可编译——lake build 通过或失败，没有中间地带；可协作——陶哲轩的观察是，传统数学合作「很少超过五名左右合著者，部分因为每位合著者都须信任并核对其他人的工作；而形式化项目经常聚集起数十名此前毫无交集的人」(Tao, 2025b)；可检索——#check、Loogle、文档站让「库里有什么」成为可查询的事实。而他那段被广泛引用的设想——向模型讲解证明，它边听边形式化为 Lean，「这是你论文的 LaTeX 版，这是你论文的 Lean 证明」(Drösser, 2024)——描绘的无非是这种文本的下一个属性：可生成。他发起泛代数项目时说的「这种范式也可用于探索新的数学，而不只是形式化已有的数学」(Tao, 2024a)，则把方向指向了生成之后的世界。

本文以一个克制的判断收束（此为作者立场）。形式化不会很快改变多数数学家的日常——第七章的账单摆在那里：因子约二十、人才数百、费马大定理以五年计。但同样由账单可见，成本曲线的方向清楚，而基础设施（库、工具链、社区）一旦建成便开始复利。第五章结尾那个对照也许值得再念一遍：最可靠的公理原来是构造的赠品。同样地，数学文本最可靠的前途，大概也不会是哪份宣言许诺的赠品——它得像每一行通过编译的代码那样，自己挣来。

参考文献

以下仅列正文中实际附有夹注的条目；网页类资源均注明访问日期（2026-09）。

← Back to 数学 & 形式

( copyright-notice )

本文为原创内容，采用 CC BY-NC-SA 4.0 协议发布。转载请注明出处并附上原文链接。

查看完整 → 网站声明

( wechat-search )

符号与连接微信搜一搜二维码

本文同步发布于微信公众号「符号与连接」。在微信搜一搜中找到我们，获取更多文章。

关注公众号 → /follow

End of Cantos