项目地址:
blog
AI 翻译:
将近 20 年前，我写了一本关于实分析的教科书，名为《分析 I》（Analysis I）。这本书旨在通过更注重基础问题（例如自然数、整数、有理数和实数的构造）来补充当时已有的许多优秀的分析教材，并提供了足够的集合论和逻辑知识，使学生能够以高度严谨的方式推导证明。
当这本书撰写时，诸如 Coq 或 Agda 这样的形式化验证工具已经存在，但我当时并未关注这一领域。然而，如今在接触了这一学科之后，我意识到本书的内容实际上与这些形式化验证系统非常契合；特别是我当时隐式使用的“朴素类型理论”（naive type theory）——用来构建标准数系的方法——与 Lean 的依赖类型理论（dependent type theory）非常匹配（其中尤其对商类型（quotient types）有着良好的支持）。
因此，我决定为《分析 I》创建一个 Lean 配套项目，该项目将书中的许多定义、定理和练习“翻译”成 Lean 代码。特别地，这提供了一种替代方式来完成书中的练习：即通过填写相应的 Lean 代码中的“sorries”。（不过，我并不计划在这个配套项目中发布官方的习题解答；你可以自由地 fork 此仓库并自行填写这些“sorries”。）
目前，以下章节内容已被翻译为 Lean：
- 第 2.1 节：自然数
- 第 2.2 节：加法
- 第 2.3 节：乘法
- 第 2 章附录：与 Mathlib 自然数的同构
- 第 3.1 节：集合论基础
- 第 4.1 节：整数
这个形式化过程中有意在某些地方脱离标准的 Lean 数学库 Mathlib，而在其他地方又依赖于它。比如，Mathlib 已经自带了自然数的标准定义 ℕ。在 Lean 的形式化中，我首先手工构造了一个不同的自然数类型 Chapter2.Nat（或简称为 Nat，如果你是在 Chapter2 命名空间下），并建立了很多关于这些新自然数的基本结果，它们与 Mathlib 中已有的一些关于 ℕ 的引理相对应（但其中很多作为练习留给读者，其证明被暂时替换为“sorries”）。然后，在附录部分，我们建立了这些新的自然数与 Mathlib 中自然数之间的同构关系（或者更准确地说，这部分也留作练习）。从那时起，“Chapter 2”中的自然数就被弃用了，转而使用 Mathlib 提供的标准自然数。我希望在整个书中延续这种模式，随着章节推进，更多地依赖 Mathlib 中的定义和函数，而不是直接引用早期章节中的替代版本。因此，这个配套项目也可以作为学习 Lean 和 Mathlib 的入门材料，同时也能帮助学习实分析（这一点有点类似于“自然数游戏”（Natural number game），事实上该游戏与我书中第 2 章在主题上有很多重叠之处）。
本仓库中的代码可以在 Lean 中编译，但我尚未测试代码中所有的（大量）“sorries”是否真的可以被填满（也就是说，这些练习是否真的能在 Lean 中被解决）。我希望能有志愿者来“试玩”这个配套项目，看看是否真的可行（以及提供的辅助引理或“API”是否足够让使用者以概念上简单明了的方式填写这些 sorries，而无需依赖一些较为冷门或复杂的 Lean 编程技巧）。当然，任何其他反馈也非常欢迎。
[更新，5 月 31 日：此配套项目已移至独立仓库。]