过渡到主流 Lean

如果你喜欢本书，也许会希望进一步使用 Lean，例如阅读 Mathematics in Lean，或启动一个独立的形式化项目。

你会发现，本书使用的 Lean“方言”不同于 mathlib 库及其相关文献（例如 Mathematics in Lean）中使用的主流数学 Lean。为了帮助你适应，本附录概述主要差异。

本书中使用的一些策略，是 mathlib 中相应策略的有意弱化版本。我这样做，是为了屏蔽 Lean 的某些能力，因为在本书层次的文字证明中，通常会把这些细节完整写出。这些有意弱化的策略包括：

表 1 本书策略及其 mathlib 原型
mathlib 策略	弱化的《证明的技艺》版本	差异
norm_num	numbers	norm_num 能完成本书要求读者手工完成的一些计算，包括模 \(n\) 化简、处理逻辑，以及检查整除性和素性
gcongr	rel	gcongr 不要求你说明正在代入哪些假设
linarith	addarith	linarith 除了加减常数外，还可以取线性不等式的常数倍；它能组合许多线性不等式，而且不要求你说明正在使用哪些假设
duper	exhaust	duper 能处理包含量词的逻辑任务，而不只限于无量词的任务

本书中使用的一些策略在 mathlib 中没有直接对应物。它们通常是对一小组引理的封装；在 mathlib 中，这些引理会按名称调用。

表 2 本书中没有 mathlib 对应物的策略
《证明的技艺》中的策略	所封装的引理
extra	Int.modEq_fac_zero、le_add_of_nonneg_right、lt_add_of_pos_right 等，以及策略 positivity
cancel	mul_left_cancel₀、lt_of_pow_lt_pow、pos_of_mul_pos_left 等，以及策略 positivity
simple_induction induction_from_starting_point two_step_induction two_step_induction_from_starting_point	Nat.le_induction、Nat.twoStepInduction 等，以及策略 induction 或 induction'

本书中的许多问题若以 mathlib 风格的 Lean 来解，会高效得多，因为某些步骤序列可以由超出本书数学范围的高级算法一步完成。应当了解的这类策略包括：

本书没有涉及的另一点，是如何与库交互。由于 mathlib 含有超过一百万行 Lean 代码，要弄清库中是否已经有你想要的引理，并不总是容易的。本书通过预先告诉你希望你使用的每个引理名称来避开这个问题。

与库交互时，需要了解以下几个基本点：

在线文档通常比源代码更易读：它可搜索，并且含有内部超链接。
引理往往以极高的一般性陈述……\((a - b) + c = a - (b - c)\) 不是针对 \(\mathbb{R}\) 陈述的，而是针对 SubtractionCommMonoid 陈述的。在修完抽象代数和点集拓扑的第一门课程之后，你可能会更容易与库交互。
如果你能猜出一个引理的精确陈述，策略 exact? 会在库中找到它。

以上只是触及皮毛：Lean 还有许多更多功能，可以帮助你进行数学探索。Mathematics in Lean、社区网站和社区讨论区提供了进一步探索的指引。祝你玩得开心！