把陶哲轩《分析》第一章到第四章搬进 Lean：teorth/analysis 到底做了什么
分析 I 的精益伴侣。例如，第 2 章发展了独立于 Mathlib 的自然数理论，但所有后续章节都将使用 Mathlib 自然数。
秒懂
- 它是什么？
- 这个仓库用 Lean 重写了《Analysis I》的前四章，刻意保留教材的叙述顺序，却牺牲了自含性来换取与 Mathlib 的兼容。它适合想学 Lean 的数学读者，不适合把形式化当效率工具的工程师。
- 适合谁用？
- 适合想通过具体数学内容学习 Lean 语法和 Mathlib 用法的读者，也适合想对照教材检查自己证明思路的人。不适合需要高效、可复用数学库的工程场景，因为代码刻意不优化效率，且大量习题以 sorry 留空。
- 能商用吗？
- 可以。Apache-2.0 是宽松许可证：你可以使用、修改并销售基于它的软件，只需保留版权和许可证声明。
- 还在维护吗？
- 在维护。仓库最近一次提交在 11 天前。
- 用什么语言写的？
- 主要是 Lean（依据 GitHub 的语言统计）。
以上回答依据项目的 GitHub 数据（最近同步于 2026年9月14日）和我们的分析，不构成法律意见。
开源项目深度解析
这个仓库解决的不是数学问题，是教学问题
它把陶哲轩《Analysis I》的前四章内容翻译成 Lean 代码。目标读者是正在读这本书、同时想学 Lean 的人。仓库不追求效率，README 直接写明 formalization is not optimized for efficiency，也不追求符合 Lean 习惯用法。它要的是尽可能贴近原书的叙述顺序，让读者在 Lean 里看到熟悉的定理和证明结构。
从自建自然数到 Mathlib 自然数的过渡机制
第 2 章用归纳类型构造自然数，完全独立于 Mathlib。第 2 章结尾的 epilogue 证明这套自建自然数与 Mathlib 的自然数同构。从第 3 章开始，所有章节直接用 Mathlib 的自然数。这个过渡是刻意的，README 说这是 sacrificing the self-containedness in favor of compatibility with Mathlib。代价是读者要在第 2 章末尾接受两套定义，好处是后面章节能直接用 Mathlib 里成熟的定理。
两处与教材不同的技术改动
第一处是序列索引从 0 开始，教材从 1 开始。原因是 Mathlib 对基于 0 的自然数支持更多。第二处是未定义运算的处理，比如除以 0 或非柯西序列的形式极限，仓库给它们赋了 junk 值如 0。README 引用了 Kevin Buzzard 的博客文章解释原因，主要是 Lean 对全函数支持更好，部分函数会引入 dependent type hell。这两处改动意味着你读代码时不能直接套用教材的直觉。
习题以 sorry 形式保留，作者明确不补
教材里留给读者的习题，在翻译中全部渲染成 sorry。作者在 README 里说欢迎 fork 仓库去尝试这些习题，但明确表示不打算把解答放进主仓库。这意味着你拿到的是一个有洞的形式化，不是完整证明。如果你是想看完整证明的读者，这个仓库会给你留下大量空白。如果你是想练习 Lean 证明的人，这些 sorry 正好是现成的练习题。
运行方式与文档入口
仓库默认分支是 main，许可证是 Apache-2.0。README 为每个章节提供了三种入口：Verso 页面、文档页面、Lean 源文件链接。例如第 2.1 节 Peano 公理的源文件是 Analysis/Section_2_1.lean，文档页面是 teorth.github.io/analysis/docs/Analysis/Section_2_1.html。要实际编译这些文件，你需要 Lean 环境和 Mathlib 依赖，但 README 没有给出具体的安装命令，仓库里也没有列出构建步骤。这一点需要你自己去 Lean 官方文档确认。
局限：教学价值与工程价值是两回事
这个仓库不适合作为数学库来用。它刻意不优化效率，定义和定理的排布服从教材叙述，不服从 Mathlib 的模块组织。如果你想在别的项目里引用这里的定理，很可能要花时间适配 Mathlib 的接口。另一个局限是覆盖范围，README 列出的章节只到第 4 章，第 1 章明确未形式化。后面章节是否存在，从材料里无法确认。如果你需要第 5 章以后的内容，这个仓库帮不上忙。
替代方案：直接学 Mathlib，或读其他形式化教材
如果你的目标不是对照陶哲轩教材，而是学会用 Lean 做数学证明，更直接的路径是学习 Mathlib 本身。Mathlib 里有大量与教材重复的定义和定理，只是定义方式略有不同。另一个替代是找专门为 Lean 初学者设计的教程项目，这类项目通常从零开始教语法，不会像这个仓库一样假定你手边有纸质教材。区别在于，teorth/analysis 的叙述顺序被教材绑死，而 Mathlib 的文档是按数学主题组织的，前者适合边读书边看代码，后者适合按需查定理。
维护成本与许可证
仓库没有最近的 release，也没有显示最后 push 时间，维护活跃度无法从材料中判断。Apache-2.0 许可证允许你 fork、修改、再分发，但要注意 README 里作者明确说不会合并习题解答。这意味着如果你补全了 sorry，你的改动会一直留在自己的分支里，无法回馈主仓库。长期看，这个项目的价值取决于它是否持续跟进 Lean 和 Mathlib 的版本更新，而这一点目前没有证据支持。
编辑结论
适合想通过具体数学内容学习 Lean 语法和 Mathlib 用法的读者，也适合想对照教材检查自己证明思路的人。不适合需要高效、可复用数学库的工程场景，因为代码刻意不优化效率，且大量习题以 sorry 留空。不适合把形式化当作教材替代品的人，README 明确说这是注解式伴侣而非替代。采用前应先确认你接受两个改动：序列从 0 开始索引，未定义运算被赋予 junk 值如 0。还要先检查你需要的章节是否已形式化，目前明确列出的是第 2 到第 4 章，第 1 章未形式化。最后，若你计划 fork 后补全习题，注意作者声明不会把解答合并回主仓库，你的成果将长期停留在自己的分支。
社区笔记