不得不感慨，陶哲轩真闲不住啊！
昨天，他还在惊叹于谷歌 DeepMind AlphaEvolve 对解决人类数学问题（比如和差集问题）起到的加速作用。更早的时候，他还开通了油管账号，当起了视频博主。
今天，陶哲轩又宣布为自己的实分析本科教材《Analysis I》创建了一个「Lean」配套项目，将教材中的各种定义、定理和练习转换成 Lean 版本，为学生提供了另一种学习方式。Lean 既是一个交互式定理证明器，也是一种编写形式化证明的语言，近些年来在数学家群体中越来越受到欢迎。
同时，陶哲轩希望该项目可以逐步过渡到标准的 Lean 库 Mathlib。Mathlib 既是 Lean 定理证明器的官方开源数学库，也是目前世界上规模最大、最活跃的形式化数学项目之一。
陶哲轩表示，大约 20 年前，他写了一本名为《Analysis I》的实分析教材，旨在补充市面上众多优秀的实分析教材。该书侧重于基础问题，例如自然数、整数、有理数和实数的构造，并提供足够的集合论和逻辑知识，使学生能够进行高度严谨的证明。
虽然在本书撰写时，Coq 或 Agda 等一些证明助手已经相当成熟，但形式化验证当时还不在陶哲轩的考虑范围内。随着现在具备了一些这方面的经验，他意识到这本书的内容实际上与这些证明助手非常兼容；特别地，之前用来构建标准数系等的「朴素类型理论」，与 Lean 的依赖类型理论（其中 Lean 对商类型的支持非常出色）非常契合。
因此，陶哲轩决定创建《Analysis I》的 Lean 配套项目，将书中的许多定义、定理和练习转换成 Lean 版本。特别地，它提供一种完成书中练习的替代方法，只需在 Lean 代码中填写对应的「待完成」（sorries）部分即可。
不过，陶哲轩不打算提供本书练习的「官方」答案。相反，他欢迎所有人自由创建这个项目的副本，并完成答题。
GitHub 地址：teorth/analysis
项目介绍
《Analysis I》共有 11 个章节，目前已被形式化的章节如下：
书籍地址：media/books/2024/05/28/1664976801.pdf
看来，陶哲轩要完成对全书的形式化，还有很多工作要做。
读者不用担心原书籍和形式化后的内容对应不上，所有章节都遵循原始书籍，根据章节序号就能找到。
需要特别说明的是，本次形式化未对运行效率进行优化，因为某些情况下转译可能不符合 Lean 的惯用规范。或许，在完成全书的工作后，陶哲轩会探索这方面的内容。
另外，原书中设置为读者练习的章节内容，在本次转译中以 sorry 占位符形式呈现。陶哲轩表示，他本人暂无计划提供习题解答。
陶哲轩还强调，尽管项目中的定义、定理及证明编排严格遵循了教材内容，但他尽量避免直接引用教材原文，而是在适当处标注了原书参考文献。因此，该形式化工程应视为原教材的注解式辅助资料，而非替代品。
Lean 版本内容截图值得强调的是，本形式化工程在设计上刻意采用了与标准数学库 Mathlib 若即若离的策略 —— 部分内容保持独立，部分则依托 Mathlib 实现。
例如，尽管 Mathlib 已具备标准自然数体系，但在第 2 章中，陶哲轩首先以手工方式构建了另一种自然数结构 Chapter2.Nat（若在 Chapter2 命名空间下可简称为 Nat），并推导出与该结构相关的基础结论。随后在结语部分，建立了这种替代自然数与 Mathlib 自然数之间的同构关系（更准确地说，是将其设为习题）。自此之后，第 2 章的自然数体系将被弃用，转而采用 Mathlib 的自然数定义。
这种先独立构建再逐步迁移的模式将贯穿全书 —— 随着章节推进，读者将越来越依赖 Mathlib 的定义与函数，而非直接引用前期章节的对应内容。
因此，本配套资料既可视为实分析的辅助教材，也能作为 Lean 与 Mathlib 的入门指南。
现在，这个 Lean 版数学副本已经上线，欢迎大家前去挑战。无论你是数学系学生、Lean 初学者，还是对形式化验证感兴趣的研究员，这都是一个亲自动手、顺便提升数学内功的好机会。而陶哲轩本人，也在等待大家的反馈。
网友评论
有熟悉陶哲轩该教材以及 Lean 的用户表示非常兴奋，希望可以移到自己的代码库中。ta 表示自己一直对数学感兴趣，而《Analysis I》是第一本真正展示如何以编程式大脑所期望的严谨方式构建数学的教材。后来也接触了 Lean，同样对其效果非常满意。
不过，Mathlib 的数学概念学习起来有点复杂，所以很高兴有人架起了从该教材到该工具的桥梁。
还有人分享了使用 Lean 来教数学的体会，最令人兴奋的地方是即时反馈。如果学生的证明错了，则根本无法通过编译。以前，学生只可以从助教、老师或其他知识渊博的专家那里获得反馈，而现在能够通过 Lean 编译器快速得到反馈。
ta 希望未来有更多选择，让 Lean 编译器提供更具指导性的反馈，就像 Rust 编译器提供代码修改建议一样。不过这可能需要专门的 LLM 才能实现。
博客地址：2025/05/31/a-lean-companion-to-analysis-i/
0 条