1. 引言

1.1. 入门指南

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

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

虽然你可以在线阅读本书的 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 是一种用于构建复杂表达式的工具，它基于一种称为 依赖类型理论 的形式语言。

每个表达式都有一个 类型，你可以使用 #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，其中 P 本身具有类型 Prop. 这样的表达式是命题 P 的证明。

theorem easy : 2 + 2 = 4 :=
  rfl

#check easy

theorem hard : FermatLastTheorem :=
  sorry

#check hard

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

这本书是一本与配套教程相辅相成的书，即 Theorem Proving in Lean， 它提供了对Lean的基础逻辑框架和核心语法更全面的介绍。 Theorem Proving in Lean 适用于那些在使用新洗碗机之前更喜欢从头到尾阅读用户手册的人。 如果你是那种更喜欢先按下 开始 按钮，以后再弄清如何启用清洗锅底功能的人，那么从本书开始更合适，需要时随时可以回去参考 Theorem Proving in Lean.

Mathematics in Lean 与 Theorem Proving in 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]⟩

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

example : ∀ m n : Nat, Even n → Even (m * n) := by
  -- Say `m` and `n` are natural numbers, and assume `n = 2 * k`.
  rintro m n ⟨k, hk⟩
  -- We need to prove `m * n` is twice a natural number. Let's show it's twice `m * k`.
  use m * k
  -- Substitute for `n`,
  rw [hk]
  -- and now it's obvious.
  ring

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

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

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

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

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

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

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

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

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

致谢. 我们感谢 Gabriel Ebner 为在 VS Code 中运行本教程搭建基础设施，以及 Kim Morrison 和 Mario Carneiro 为把本教程迁移到 Lean 4 提供的帮助。 我们还感谢 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, Joseph McKinsey, Bhavik Mehta, Isaiah Mindich, Kabelo Moiloa, Hunter Monroe, Pietro Monticone, Oliver Nash, Emanuelle Natale, Filippo A. E. Nuccio, Pim Otte, Bartosz Piotrowski, Nicolas Rolland, Keith Rush, Yannick Seurin, Guilherme Silva, Bernardo Subercaseaux, Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker, Floris van Doorn, Eric Wieser 等人提供的帮助和修正。 我们的工作部分得到了Hoskinson Center for Formal Mathematics的支持。