1. 引言

1.1. 入门指南

本书教你使用 Lean 4 交互式证明助手来形式化数学。你需要一点儿数学知识，但并不需要太多。 我们将涵盖从数论到测度论和分析的基础方面，如果你对它们不熟悉，你可以在学习的过程中逐渐掌握。 我们也不预设任何对形式化方法的背景知识。 形式化可以被视为一种计算机编程：我们将用一种 Lean 可以理解的规范化的语言，类似于编程语言，来编写数学定义、定理和证明。 作为回报，Lean 提供反馈和信息，解析表达式并保证它们是形式良好的，并最终验证我们的证明的正确性。

你可以从 Lean 项目页面 和 Lean 社区网页 了解更多关于 Lean 的信息。本教程基于 Lean 庞大且不断增长的库 Mathlib。 我们也强烈建议加入 Lean Zulip 在线聊天群，如果你还没有加入的话。 在那里你会发现一个活跃而友好的 Lean 爱好者社区，愿意回答问题并提供精神支持。

  • 项目在Mathlib版本 15a391f3007c5c377ba21af3e0a1d53502310685 上测试通过（2024.10.16）。Mathlib 更新迅速，可能会遇到旧版代码在新版 Mathlib 下无法通过的问题。如果读者遇到了版本不兼容问题，请提交PR以使本项目跟进最新 Mathlib，或者提交issue或联系译者协助解决。

虽然你可以在线阅读本书的 pdf （注：中文版暂不支持 pdf） 或 html 版本，但它设计为可以交互式阅读，在 VS Code 编辑器中运行 Lean 代码。开始学习吧：

（中文用户可以参考 中文安装教程 ）

  1. 按照这些 安装说明 安装 Lean 4 和 VS Code.

  2. 确保你已安装了 git.

  3. 按照这些 说明 来获取 mathematics_in_lean 存储库并在 VS Code 中打开它。

4. 本书的每个部分都有一个与之相关联的 Lean 文件，其中包含示例和练习。你可以在名为 MIL 的文件夹中按章节组织的地方找到它们。 我们强烈建议复制该文件夹，并在复制的文件夹中进行实验和练习。这样可以保持原始文件的完整性，并且在存储库改动时更容易同步（见下文）。 你可以将复制的文件夹命名为 my_files 或其他任何你喜欢的名字，并在其中创建自己的 Lean 文件。

在这之后，你可以按照以下步骤在 VS Code 的侧边栏中打开教科书：

  1. 输入 ctrl-shift-P （在 macOS 中为 command-shift-P ）。

  2. 在出现的栏中输入 Lean 4: Docs: Show Documentation Resources，然后按回车键。（一旦该选项在菜单中被高亮显示，你就可以按回车键选择它。）

  3. 在打开的窗口中，点击 Mathematics in Lean.

或者，你还可以在云中运行 Lean 和 VS Code，使用 Gitpod。 你可以在 Github 上的 Mathematics in Lean 项目官方页面 或 中文页面 找到如何操作的说明。 尽管如此，我们仍然建议按照上述方式在 MIL 文件夹的副本中进行操作。

这本教科书及其相关存储库仍在不断完善中。你可以通过在 mathematics_in_lean 文件夹内输入 git pull, 接着输入 lake exe cache get 来更新存储库。（这假设你没有改变 MIL 文件夹的内容，这也是我们建议你制作副本的原因。）

我们希望你在阅读教科书的同时，在 MIL 文件夹中完成练习，该文件夹包含了解释、说明和提示。文本通常会包含示例，就像这个例子一样：

#eval "Hello, World!"

你应该能够在相关的 Lean 文件中找到相应的示例。如果你点击该行，VS Code 将在 Lean Goal 窗口中显示 Lean 的反馈， 如果你将光标悬停在 #eval 命令上，VS Code 将在弹出窗口中显示 Lean 对此命令的响应。我们鼓励你编辑文件并尝试自己的示例。

此外，本书还提供了许多具有挑战性的练习供你尝试。不要匆忙跳过这些练习！Lean 需要*交互式地做*数学，而不仅仅是阅读。 完成练习是学习的核心内容。你不必完成所有练习；当你觉得已经掌握了相关技能时，可以自由地继续前进。 你始终可以将你的解决方案与与每个部分相关的 solutions 文件夹中的解决方案进行比较。

1.2. 概述

简言之，Lean 是用于构建复杂表达式的工具，它基于一种称为 依值类型论（Dependent type theory） 的形式语言。

每个表达式都有一个 类型（Type），你可以使用 #check 命令来打印它。一些数学对象表达式的类型可能是像 ℕ 或 ℕ → ℕ 这样的。

#check 2 + 2

def f (x : ℕ) :=
  x + 3

#check f

数学命题的类型是 Prop。

#check 2 + 2 = 4

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

#check FermatLastTheorem

设命题 P 类型为 Prop，你可以构造类型为 P 的表达式，它们是命题 P 的证明。

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

如果你设法构建了一个类型为 FermatLastTheorem 的表达式，并且 Lean 接受它作为该类型的项，那么你已经干了一件伟大的事。 （使用 sorry 是作弊，Lean 知道这一点。）所以现在你知道了游戏目标。剩下要学习的只有规则了。

本书配套教程 Theorem Proving in Lean，中文版 Lean 中的定理证明，提供了对Lean的基础逻辑框架和核心语法更全面的介绍。 Lean 中的定理证明适用于那些在使用新洗碗机之前更喜欢从头到尾阅读用户手册的人。 如果你是那种更喜欢先动手尝试，以后再弄清细节的人，那么从本书开始更合适，需要时随时可以回去参考 Lean 中的定理证明。

Lean 形式化数学与 Lean 中的定理证明的另一个区别在于，本书更加强调 证明策略(Tactics) 的使用。 考虑到我们试图构建复杂表达式，Lean 提供了两种方法：直接构造表达式本身，或者向 Lean 提供 指令，告诉它如何构建这些表达式。 例如，下面构造的证明表达式在说明，如果 n 是偶数，则 m * n 也是偶数：

example : ∀ m n : Nat, Even n → Even (m * n) := fun m n ⟨k, (hk : n = k + k)⟩ ↦
  have hmn : m * n = m * k + m * k := by rw [hk, mul_add]
  show ∃ l, m * n = l + l from ⟨_, hmn⟩

这个 证明项 可以压缩成一行：

example : ∀ m n : Nat, Even n → Even (m * n) :=
fun m n ⟨k, hk⟩ ↦ ⟨m * k, by rw [hk, mul_add]⟩

以下是同一定理的策略式证明，其中以 -- 开头的行是注释，因此被 Lean 忽略：

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- 设 `m` 和 `n` 是自然数，设 `n = 2 * k`
  rintro m n ⟨k, hk⟩
  -- 需证 `m * n` 是某自然数的两倍。那就设它是 `m * k` 的两倍吧
  use m * k
  -- 代入 `n`
  rw [hk]
  -- 剩下的就很显然了
  ring

当你在 VS Code 中输入上述证明的每一行时，Lean 会在一个单独的窗口中显示 证明状态，告诉你已经建立了哪些事实，以及要证明你的定理还需要完成什么任务。 你可以通过逐行逐步骤回顾证明，因为 Lean 将继续显示光标所在点的证明状态。 本例中，证明的第一行引入了 m 和 n （此时可以重命名它们，如果我们想的话），并且将假设 Even n 分解为 k 和假设 n = 2 * k. 第二行， use m * k, 声明我们将通过证明 m * n = 2 * (m * k) 来证明 m * n 是偶数。 下一行使用了 rewrite 策略在目标中将 n 替换为 2 * k，得到的新目标 m * (2 * k) = 2 * (m * k) 最终被 ring 策略解决。

逐步构建证明并获得增量反馈的能力非常强大。因此，策略证明通常比编写证明项更容易也更快。两者之间没有明显的区别：策略证明可以插入到证明项中， 就像我们在上面的例子中使用短语 by rw [hk, mul_left_comm] 一样。我们还将看到，反之，将一个简短的证明项插入到策略证明中通常也很有用。 虽然如此，但在这本书中，我们会把重点放在策略的使用上。

在我们的例子中，策略证明也可以简化为一行：

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩; use m * k; rw [hk]; ring

在这里，我们使用策略来执行每个细节证明步骤。但是 Lean 提供实质性的自动化，并且可以证明更长的计算和更大的推理步骤。 例如，我们可以使用特定的规则调用 Lean 的化简器，用于化简关于奇偶性的语句，以自动证明我们的定理。

example : ∀ m n : Nat, Even n → Even (m * n) := by
  intros; simp [*, parity_simps]

两本入门教程之间的另一个重大区别是，Lean 中的定理证明仅依赖于 Lean 内核以及其内置的策略，而 Lean 形式化数学建立在 Lean 强大且不断增长的库 Mathlib 的基础上。 因此，我们会向您展示如何使用库中的一些数学对象和定理，以及一些非常有用的策略。 这本书无意用于对库进行完整描述； 社区 网页包含了详尽的文档。 不如说，本入门教程是向您介绍形式化背后的思维风格，让您可以轻松浏览库并自行查找内容。

交互式定理证明可能会令人沮丧，学习曲线很陡峭。但是 Lean 社区非常欢迎新人，而且任何时间都有人在 Lean Zulip 聊天群 上在线回答问题。 我们希望能在那里见到你，并且毫无疑问，很快你也将能够回答这类问题并为 Mathlib 的发展做出贡献。

因此，如果你选择接受这个任务，你的使命如下：投入其中，尝试练习，有问题就来 Zulip 提问，并享受乐趣。 但要注意：交互式定理证明将挑战你以全新的方式思考数学和进行数学推理。这可能改变你的生活。

致谢. Acknowledgments. We are grateful to Gabriel Ebner for setting up the infrastructure for running this tutorial in VS Code, and to Kim Morrison and Mario Carneiro for help porting it from Lean 4. We are also grateful for help and corrections from Takeshi Abe, Julian Berman, Alex Best, Thomas Browning, Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin, Mark Czubin, Alexandru Duca, Pierpaolo Frasa, Denis Gorbachev, Winston de Greef, Mathieu Guay-Paquet, Marc Huisinga, Benjamin Jones, Julian Külshammer, Victor Liu, Jimmy Lu, Martin C. Martin, Giovanni Mascellani, John McDowell, Isaiah Mindich, Hunter Monroe, Pietro Monticone, Oliver Nash, Emanuelle Natale, Pim Otte, Bartosz Piotrowski, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva, Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker, Floris van Doorn, Eric Wieser, and others. Our work has been partially supported by the Hoskinson Center for Formal Mathematics.

感谢 `Lean-zh 中文社区<https://www.leanprover.cn/>`_ 的伙伴们参与译本的创作和校对。