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

项目地址:

\n\n

blog

\n\n

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 日：此配套项目已移至独立仓库。]

\n","createdAt":"2025-06-03 19:31:07.327843","updatedAt":"2025-06-03 19:31:07.327843","replyToPostNumber":null,"replyCount":0,"likeCount":3,"wordCount":1038,"liked":false,"bookmarked":false,"polls":[],"reactions":[{"reaction":"❤️","count":3,"users":[{"id":2877,"username":"Zerick","name":null},{"id":3003,"username":"welldown","name":"Jerry"},{"id":5905,"username":"PipaQinse233","name":"PipaQinse233"}],"hasReacted":false}],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"isAnonymous":false,"user":{"id":4668,"username":"IO","name":null,"avatarUrl":null,"admin":true,"moderator":false,"signatureRaw":"","signatureCooked":null}},{"id":54515,"postNumber":2,"raw":"https://www.youtube.com/@TerenceTao27\n\n最近也是传了一些 Lean 的视频教程","cooked":"\n

最近也是传了一些 Lean 的视频教程

\n","createdAt":"2025-06-03 19:52:01.021002","updatedAt":"2025-06-03 19:52:01.021002","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":15,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"isAnonymous":false,"user":{"id":4668,"username":"IO","name":null,"avatarUrl":null,"admin":true,"moderator":false,"signatureRaw":"","signatureCooked":null}}],"hasMore":false,"lastReadPostNumber":1,"hasUrlPostNumber":true}