前言

关于本书

本书讨论如何书写细致而严谨的数学证明。本书配有以计算机形式化语言 Lean 写成的代码。

本书关注的是证明技巧，而不是理论体系的建立：书中证明后还会在后文反复引用的定理并不多。相反，本书的核心在于例题。正文中有两百多个带解答的问题作为例题，另有数百个无解答的问题留给读者练习。每个问题和每个解答都同时以标准数学文字和 Lean 呈现（阅读本书时，应在计算机上打开相应的 Lean 代码文件）；而对于刚接触证明的学生来说，这两种“语言”几乎同样陌生，因此大多数解答都附有非形式化的说明。

为什么使用 Lean？

几千年来，人们一直用文字表达数学论证。如今数学语言已经高度标准化，并形成了许多约定，使数学家能够高效而无歧义地相互交流。本书的首要目标，是教你阅读和书写标准的数学英文文字。

称为交互式定理证明器的计算机系统（也称为证明助理，或用于形式化的系统）提供了表达数学论证的另一种方式。Lean 是其中一种系统；它是一个开源项目，自 2013 年以来由 Microsoft Research 等机构开发。不过，这类系统早在计算机发展的早期就已经出现。

像 Lean 这样的交互式定理证明系统多年来已经变得越来越容易使用，但它们还远谈不上真正容易使用：它们会像其他程序设计语言一样挑剔而严格。那么，为什么本书建议你在第一次接触证明时就使用这样的系统呢？

第一，如其名称所示，在交互式定理证明器中书写证明是交互式的。在证明的每个时刻，你都可以看到证明状态的可视化表示：你已经知道什么（你的假设），以及你当前要证明什么（你的目标）。如果你刚开始书写数学证明，可能会惊讶地发现，在纸上经历几步正向推理和反向推理的交替之后，区分假设与目标并不容易；在分类讨论中，也很容易忘记某一个情形。Lean 实时更新的证明状态表示，使你不必把这些信息全部放在工作记忆中。

第二，计算机形式化系统毕竟是严格而不宽容的程序设计语言；你一犯错，它们就会给出语法错误。反馈是即时的，你可以不断迭代，直到得到可运行的内容。用 Lean 写出的解答保证是完全正确的：不会在负号下错误地代换不等式，不会除以零，也不会在代数运算中漏掉项。这对于证明型数学尤其有用：在微积分题中，若中途犯一个小错，后面的解答也许改动不大；但在证明中途犯一个小错，后面的论证可能就完全失效。

最后，你通过策略与 Lean 交互；每个策略执行某种推理方式中的一个步骤。本教材教授的策略（其中一些是为本书专门编写的）各自构成本书心智世界中一个允许使用的推理“原子”。这使得一件在纯文字教材中可能带有主观性的事情变得客观：什么算作一个细节完整的证明。不仅如此，我提供给你的这些“原子”也被设计成会引导你采用某些数学论证结构风格1；这些风格在标准数学文字中是惯常的，但学生往往需要较长时间才能自然采用。

本书是一部以 Lean 为工具的数学教材。它的设计目标是让 Lean 的学习曲线比数学本身更平缓2：这部分依靠精心选择的练习，部分依靠使用我自己的一种 Lean“方言”，其中 Lean 词汇表3受到限制，但又刚好足以满足本书的数学需要。（主要差异的摘要可见附录过渡到主流 Lean。）我希望，在解题时，你的大部分智力努力都用于数学本身，而不是用于 Lean 的实现细节或语法怪癖。

内容与预备知识

如果你（1）非常熟悉高中代数，并且（2）有学习执行复杂数学算法的经验，那么你已经准备好阅读本书了。我心目中的典型读者，是刚学完 Calculus II 的大学一、二年级学生。但本书实际上不使用微积分。

本书最主要的新意是“双语”呈现：把文字数学与 Lean 代码并列。但这种呈现方式所要求的设计选择，也在其他方面塑造了本书。

第 1 章对“计算式证明”作了格外细致的处理。这样的证明之所以自然地成为本书起点，是因为它们很容易翻译成 Lean；但它们本身也值得重视，因为这一层次的学生常常会在这类问题上遇到困难。4

第 2 章和第 4 章缓慢推进自然演绎规则，解决关于 \(\mathbb{N}\)、\(\mathbb{Z}\)、\(\mathbb{Q}\) 和 \(\mathbb{R}\) 的问题；这些问题逐渐包含越来越多的逻辑联结词和量词。把一切都翻译成 Lean 的要求，使本书在这些章节中保持严格诚实。典型的入门证明教材没有这道护栏，因此常会出现一些小的越界之处，例如给出一个很好的分类证明例子，但其中暗中使用了尚未讲到的证明技巧，如为存在命题补上见证。

逻辑直到第 5 章才被明确讲授；到那时，读者已经熟悉各种逻辑联结词和量词，也熟悉在文字与符号之间来回翻译数学陈述。因此，逻辑章可以相对简短，并把重点放在逻辑等价这一概念上（主要用自然演绎来呈现，以便与第 2 章和第 4 章衔接，而不是使用真值表）。5

本书其余章节更接近第一门证明课程通常会覆盖的内容。此时读者已经对 Lean 足够熟悉，数学呈现也不再受到限制。

第 3 章讨论初等数论的基本概念。该章只使用有限的推理工具，因此可以放在第 2 章和第 4 章之间作为间歇。后续章节中还会继续以数论定义和定理作为例子，而数论部分则在第 7 章以希腊数学的大结果作结：素数有无穷多个、欧几里得引理以及二的平方根为无理数。

第 6 章讨论归纳法。处理相当全面，包括相对于 \(\mathbb{Z}\)、\(\mathbb{N}\times \mathbb{N}\) 和 \(\mathbb{Z}\times \mathbb{Z}\) 上各种非平凡良基关系的归纳与递归。

最后，第 8 章、第 9 章和第 10 章依次讨论函数、集合和关系。我们采取类型论观点：函数是原始概念，而集合和关系则被定义为取值于 \(\left[\operatorname{true}/\operatorname{false}\right]\) 的函数。

教师说明

本书基于我在 2023 年春季于 Fordham University 教授的一门课程的讲义。该课程有 20 名学生，主要是一、二年级学生，其中位背景是 Calculus II。许多学生（但并非全部）也修过一门计算机编程入门课。

这门课每周两次，每次 75 分钟，共 13 周；在这段时间里覆盖了本书约 80% 的内容。一次典型课堂结构可能如下：

25 分钟传统黑板讲授；
5 分钟屏幕共享讲授，在 Lean 中做同样的问题；
20 分钟学生两人一组在 Lean 中练习，教师巡视；
25 分钟传统黑板讲授，也许比前一段更偏理论。

这门课的作业可按需提供。作业相对较短（每周 5 到 7 题），但学生几乎必须同时以书面和 Lean 两种形式提交所有题目。大多数学生需要在办公时间或通过电子邮件获得支持，才能完成这些作业。

课程还在第 5 周和第 10 周设置了口试。这些是一对一的 20 分钟面试，用来评估 Lean 熟练度：学生现场解决此前未见过的 Lean 练习（每位学生的题目不同），并口头解释自己的推理。课程成绩构成为：作业 25%，口试 20%，传统笔试 55%（一次期中和一次期末，二者完全不含 Lean）。

显然，课堂中教师巡视指导、办公时间和邮件中的作业支持、以及口试相结合，意味着需要花相当多时间与单个学生（或小组学生）互动。学生与教师 20:1 的比例是可持续的。我怀疑若要超过这一比例，就需要非常强的学生，或一位有经验且热情高涨的助教。

学生们在云端开发环境中运行 Lean，以免需要在自己的计算机上安装 Lean。我使用的是 Gitpod（另一种选择是 GitHub Codespaces）；如何开始使用 Gitpod，可参见本书代码仓库 README 中的简短说明。学生的 Lean 作业通过 Gradescope 自动评分器自动评分（另一种选择是 GitHub Classroom）。Lean 社区的教学建议网页提供了搭建这类课程基础设施的说明和故障排查。

致谢

我由衷感谢

Microsoft Research 提供了资助，支持本书写作；
Fordham 的本系允许我教授这门发展出本书的实验课程；
该课程 Math 2001 L01 Spring 2023 中勇敢尝试的学生们，感谢他们的热情与机智；
Matthew Hertz 搭建了本书的 Sphinx 基础设施，并排版了最初几章；
mathlib 社区，特别是 Mario Carneiro、Gabriel Ebner、Scott Morrison、Thomas Murrills 和 David Renshaw，感谢他们在 2022 年秋至 2023 年冬进行 Lean 3 到 Lean 4 移植时，优先处理我课程所需的库内容；
Mario Carneiro 还参与了多次长时间编程攻关，产出了本书中最有意思的一些定制策略；
Jeremy Avigad、Rob Lewis 和 Patrick Massot 分享了 Lean 课程的技术基础设施，并与我多次讨论用 Lean 教授数学这一梦想。

脚注

1: 例如，在大多数代数推理中使用计算块，以及偏好正向推理而不是反向推理。
2: 如果你想要相反方向的教材，Mathematics in Lean 是数学化 Lean 的标准入门书。但请注意，那本书预期读者有更多数学经验：即使只是证明初等命题，书写惯用的 Lean 代码也需要一定的数学成熟度。
3: 用于代数推理的策略词汇包括 ring、rw、numbers（即 norm_num）、rel（为本书定制编写，但现在已进入 mathlib 正式库）、extra（定制编写）和 cancel（定制编写）。它们足以处理整数上几乎所有代数推理，包括非线性不等式。本书在第 1.2 节到第 2.1 节中训练这种语汇，后来会带来回报：它避免了按名称调用无穷无尽的引理，例如 mul_le_mul_of_nonneg_left、pow_pos 或 le_of_pow_le_pow。其他定制自动化也会轻量地简化归纳原理、良基性证明、积类型和集合方面的工作。全书中按名称调用的引理总数不到五十个。
4: 事实上，在许多入门证明课程中，即使没有真正掌握这种推理方式，也完全有可能应付大量以等式为主的推理；但若不掌握计算式证明，几乎不可能熟练处理不等式。如果学生没有在入门证明课程中学会这一技巧，那么到实分析时，它会重新回来成为障碍。
5: 有经验的读者也许会喜欢第 5.2 节中的问题；该节引入经典推理。这些问题（据我所知）是新的，而且比通常教材中的例子更初等。