陶哲轩（Terence Tao）的《Analysis I》Lean 形式化项目
这个 GitHub 仓库 是陶哲轩于2025 年 5 月 31 日正式启动的一个开源项目，目的是将他的经典实分析教材《Analysis I》（本科生水平）用Lean 4证明助手进行形式化翻译。
项目核心目标
- 忠实复述原书：尽可能贴近教材的定义、定理和证明结构，同时展示 Lean 的语法和特性（不追求最高效率，有时会偏离 Lean 的“习惯用法”）。
- 作为伴侣资源：不是取代原书，而是提供一个“带注释的伴侣”。书中留给读者的习题在这里用
sorry（占位符）表示，鼓励读者自己 fork 仓库填写证明。 - 不直接引用原书文字：只给出原书章节引用，避免版权问题。
- 与 Mathlib 兼容：早期章节独立定义（如第 2 章自己构建自然数），后期逐步切换到 Lean 标准数学库Mathlib的定义（并在章节结尾证明两者同构），这样既教学又实用。
技术调整（为什么与原书稍有不同）
- 序列从0 开始索引（原书从 1 开始），因为 Mathlib 对ℕ（从 0 开始）的支持更好。
- 一些原书未定义的操作（如除以 0、非 Cauchy 序列的极限）被赋“垃圾值”（如 0），确保函数是全定义的（total function）。Lean 对全函数支持更好，避免部分函数带来的证明复杂性（“dependent type hell”）。
- 第 2 章自然数用归纳类型构造（而非纯公理化），但在结尾证明了 Peano 公理。
当前形式化进度（截至 2025 年 12 月）
项目进展非常快，已基本覆盖全书主要内容（第 1 章引言未形式化）：
- 第 2 章：自然数（Peano 公理、加法、乘法）+ 与 Mathlib 同构。
- 第 3 章：集合论基础、函数、像与原像、笛卡尔积、基数等。
- 第 4 章：整数、有理数、绝对值、指数、理性数的间隙。
- 第 5 章：实数构造（Cauchy 序列）、序、最小上界界、实指数等 + 与 Mathlib 实数同构。
- 第 6 章：序列极限、扩展实数、上下极限、标准极限、子序列等。
- 第 7 章：级数（有限、无限、非负和、重排、根检验/比检验）。
- 第 8 章：无穷集合（可数、不可数、选择公理、有序集）。
- 第 9 章：ℝ上连续函数（子集、极限、连续性、中值定理、一致连续等）。
- 第 10 章：导数（基本定义、单调性、反函数导数、L’Hôpital 法则）。
- 第 11 章：Riemann 积分（分划、上/下积分、可积性、基本定理等）。
- 附录 A：数学逻辑基础（语句、蕴涵、量词、相等等）。
- 附录 B：十进制表示。
此外，还有一些额外内容：
- 陶哲轩的《测度论》书籍形式化（进行中）。
- 物理单位系统形式化（包括 SI 单位）。
- 有限选择公理（避免使用 Lean 的选择公理）。
- 有限概率论及几个 Erdős 问题的解。
项目现状与影响
- 社区活跃：1.4k 星、181 fork、36 位贡献者，最近提交在几天前。
- 文档网站：Partial Lean formalization of Analysis I — Verso （每个章节有 Verso 页面、文档和 Lean 源代码）。
- 资源：仓库提供构建脚本、Lean 社区链接、Mathlib 搜索工具等。陶哲轩的 YouTube 频道有相关演示。
- 这体现了陶哲轩对 AI+ 证明助手的乐观态度：项目中使用 GitHub Copilot 等工具加速形式化，正如他之前预测的，AI 正让形式验证变得更易普及。
这个项目不仅是《Analysis I》的“机器可验证版本”，还是学习 Lean 和 Mathlib 的绝佳入门材料，尤其适合想结合教材和形式化证明的学生/研究者。如果你感兴趣，可以直接 clone 仓库尝试填写 sorry 部分！