.. raw:: latex

    \frontmatter

.. _introduction:

前言
====

关于本书
--------

本书讨论如何书写细致而严谨的数学证明。本书配有以计算机形式化语言
`Lean <https://leanprover.github.io/about/>`__ 写成的代码。

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


为什么使用 Lean？
----------------

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

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

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

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

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

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

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

内容与预备知识
--------------

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

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

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

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

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

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

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

:numref:`第 %s 章 <induction>` 讨论归纳法。其处理相当全面，包括相对于
:math:`\mathbb{Z}`、:math:`\mathbb{N}\times \mathbb{N}` 和
:math:`\mathbb{Z}\times \mathbb{Z}` 上各种非平凡良基关系的归纳与递归。

最后，:numref:`第 %s 章 <functions>`、:numref:`第 %s 章 <sets>` 和
:numref:`第 %s 章 <relations>` 依次讨论函数、集合和关系。我们采取类型论观点：
函数是原始概念，而集合和关系则被定义为取值于
:math:`\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 <https://www.gitpod.io/>`_（另一种选择是
`GitHub Codespaces <https://github.com/features/codespaces>`_）；如何开始使用 Gitpod，
可参见本书 `代码仓库 <https://github.com/hrmacbeth/math2001>`_ README 中的简短说明。
学生的 Lean 作业通过 `Gradescope <https://www.gradescope.com/>`_ 自动评分器自动评分
（另一种选择是 `GitHub Classroom <https://classroom.github.com/>`_）。
Lean 社区的 `教学建议网页 <https://leanprover-community.github.io/teaching/>`_
提供了搭建这类课程基础设施的说明和故障排查。

致谢
----

我由衷感谢

* Microsoft Research 提供了 `资助 <https://www.microsoft.com/en-us/research/academic-program/microsoft-research-lean-award-program/>`_，
  支持本书写作；
* Fordham 的本系允许我教授这门发展出本书的实验课程；
* 该课程 Math 2001 L01 Spring 2023 中勇敢尝试的学生们，感谢他们的热情与机智；
* Matthew Hertz 搭建了本书的 Sphinx 基础设施，并排版了最初几章；
* `mathlib 社区 <https://leanprover-community.github.io/>`_，特别是 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 教授数学这一梦想。

.. rubric:: 脚注

.. [#] 例如，在大多数代数推理中使用计算块，以及偏好正向推理而不是反向推理。

.. [#] 如果你想要相反方向的教材，
  `Mathematics in Lean <https://leanprover-community.github.io/mathematics_in_lean/>`_
  是数学化 Lean 的标准入门书。但请注意，那本书预期读者有更多数学经验：
  即使只是证明初等命题，书写惯用的 Lean 代码也需要一定的数学成熟度。

.. [#] 用于代数推理的策略词汇包括 ``ring``、``rw``、
  ``numbers``（即 ``norm_num``）、``rel``（为本书定制编写，但现在已进入 mathlib 正式库）、
  ``extra``（定制编写）和 ``cancel``（定制编写）。它们足以处理整数上几乎所有代数推理，
  包括非线性不等式。本书在 :numref:`第 %s 节 <proving_equalities_in_lean>` 到
  :numref:`第 %s 节 <tactic_mode>` 中训练这种语汇，后来会带来回报：
  它避免了按名称调用无穷无尽的引理，例如 ``mul_le_mul_of_nonneg_left``、``pow_pos`` 或
  ``le_of_pow_le_pow``。其他定制自动化也会轻量地简化归纳原理、良基性证明、积类型和集合方面的工作。
  全书中按名称调用的引理总数不到五十个。

.. [#] 事实上，在许多入门证明课程中，即使没有真正掌握这种推理方式，
  也完全有可能应付大量以 *等式* 为主的推理；但若不掌握计算式证明，几乎不可能熟练处理 *不等式*。
  如果学生没有在入门证明课程中学会这一技巧，那么到实分析时，它会重新回来成为障碍。

.. [#] 有经验的读者也许会喜欢 :numref:`第 %s 节 <lem>` 中的问题；该节引入经典推理。
  这些问题（据我所知）是新的，而且比通常教材中的例子更初等。