“分析 I”的精益伴侣 - SegmentFault 思否

近 20 年前，作者写了一本名为“Analysis I”的实分析教科书，旨在补充现有的许多优秀分析教科书，更注重基础问题，如自然数、整数、有理数和实数的构造，以及提供足够的集合论和逻辑，让学生能够进行高水平的严格证明。
写这本书时，像 Coq 或 Agda 这样的一些证明助手已经很成熟，但形式验证当时不在作者的考虑范围内。现在有了相关经验后，作者意识到这本书的内容实际上与这些证明助手非常兼容，特别是作者隐含使用的“朴素类型理论”与 Lean 的依赖类型理论非常吻合，Lean 对商类型有很好的支持。
因此，作者决定推出一个“Analysis I”的 Lean 伴侣，这是将文本中的许多定义、定理和练习翻译成 Lean 的“翻译”。通过在 Lean 代码中填写相应的“抱歉”，可以提供一种执行书中练习的替代方法，但作者不打算在这个伴侣中提供“官方”的练习解决方案，欢迎创建包含填写好的“抱歉”的存储库分支。
目前，文本的以下部分已翻译成 Lean：
形式化在某些地方故意与标准 Lean 数学库Mathlib分离，但在其他地方依赖它。例如，Mathlib 已经有自然数 ${{\bf N}}$ 的标准概念。在 Lean 形式化中，作者首先“手动”开发自然数的另一种构造Chapter2.Nat（或在Chapter2命名空间中为Nat），建立关于这些替代自然数的许多基本结果，这些结果与 Mathlib 中已有的 ${{\bf N}}$ 的类似引理平行（但其中许多引理作为练习留给读者，目前用“抱歉”代替证明）。然后，在一个结语部分，建立这些替代自然数与 Mathlib 自然数之间的同构（或更确切地说，作为练习）。从那时起，第二章的自然数被弃用，而使用 Mathlib 自然数。作者打算在整本书中继续这种一般模式，以便随着进入后面的章节，越来越依赖 Mathlib 的定义和函数，而不是直接引用早期章节的任何对应部分。因此，这个伴侣也可以用作 Lean 和 Mathlib 以及实分析的介绍（在某种程度上类似于“Natural number game”，实际上与作者文本的第二章有很大的主题重叠）。
存储库中的代码在 Lean 中可以编译，但作者尚未测试代码中的所有（众多）“抱歉”是否实际上可以被填充（即所有练习是否实际上可以在 Lean 中解决）。作者希望有志愿者“试玩”这个伴侣，看看是否可以做到（以及 Lean 文件中提供的辅助引理或“API”是否足以以概念上简单的方式填充“抱歉”，而不必依赖更神秘的 Lean 编程技术）。当然，也欢迎其他反馈。
[更新，5 月 31 日：将伴侣移到一个独立的存储库中。]