陶哲轩：感谢Lean，我又重写了20年前经典教材！
文章摘要
陶哲轩近日宣布为其本科教材《Analysis I》创建了一个Lean配套项目，将书中的定义、定理和练习转换为Lean版本，为学生提供了一种新的学习方式。Lean是一种交互式定理证明器和编写形式化证明的语言，近年来在数学家中越来越受欢迎。陶哲轩希望该项目能逐步过渡到标准的Lean库Mathlib，这是目前世界上规模最大、最活跃的形式化数学项目之一。
《Analysis I》是一本实分析教材，侧重于基础问题，如自然数、整数、有理数和实数的构造，并提供足够的集合论和逻辑知识，使学生能够进行高度严谨的证明。虽然该书在撰写时未考虑形式化验证，但陶哲轩现在意识到其内容与Lean等证明助手非常兼容。因此，他决定创建Lean配套项目，将书中的许多定义、定理和练习转换为Lean版本，并提供一种完成书中练习的替代方法。
陶哲轩不打算提供本书练习的“官方”答案，而是欢迎所有人自由创建项目副本并完成答题。该项目目前已完成部分章节的形式化，所有章节都遵循原始书籍，根据章节序号就能找到对应内容。需要注意的是，本次形式化未对运行效率进行优化，某些情况下转译可能不符合Lean的惯用规范。此外，原书中设置为读者练习的章节内容在本次转译中以sorry占位符形式呈现，陶哲轩暂无计划提供习题解答。
该形式化工程应视为原教材的注解式辅助资料，而非替代品。在设计上，该项目采用了与标准数学库Mathlib若即若离的策略，部分内容保持独立，部分则依托Mathlib实现。例如，尽管Mathlib已具备标准自然数体系，但在第2章中，陶哲轩首先以手工方式构建了另一种自然数结构，并推导出与该结构相关的基础结论，随后在结语部分建立了这种替代自然数与Mathlib自然数之间的同构关系。这种先独立构建再逐步迁移的模式将贯穿全书，随着章节推进，读者将越来越依赖Mathlib的定义与函数。
本配套资料既可视为实分析的辅助教材，也能作为Lean与Mathlib的入门指南。现在，这个Lean版数学副本已经上线，欢迎数学系学生、Lean初学者以及对形式化验证感兴趣的研究员前去挑战。陶哲轩本人也在等待大家的反馈。有熟悉陶哲轩该教材以及Lean的用户表示非常兴奋，希望可以移到自己的代码库中，并认为《Analysis I》是第一本真正展示如何以编程式大脑所期望的严谨方式构建数学的教材。此外，还有人分享了使用Lean来教数学的体会，最令人兴奋的地方是即时反馈，如果学生的证明错了，则根本无法通过编译，这为学习提供了极大的便利。
原文和模型
【原文链接】 阅读原文 [ 1575字 | 7分钟 ]
【原文作者】 机器之心
【摘要模型】 deepseek-v3
【摘要评分】 ★★★☆☆
相关文章
