文章摘要
陶哲轩最近对形式化数学证明产生了浓厚兴趣，并在YouTube上开设了账号，上传了四段视频，专门介绍如何使用Lean进行形式化数学证明。其中，第三支视频尤为引人注目，他借助GitHub Copilot挑战了微积分中的ε-δ极限问题。这一系列视频不仅展示了他对形式化验证的热情，也为数学学习者提供了全新的学习途径。
陶哲轩还启动了一个新的开源项目，旨在将他经典的数学分析教材《Analysis I》中的定义、定理和习题翻译成Lean语言。这本教材自2006年首次出版以来，已成为数学分析领域的经典之作，多次更新并广受欢迎。通过将教材内容形式化，陶哲轩希望为学生提供一种不同于传统纸笔推演的学习方式，使他们能够通过编写Lean代码来完成数学证明。
《Analysis I》的内容从数系结构和集合论开始，逐步深入到幂级数、多元微分学和傅里叶分析，最后介绍勒贝格积分。全书以实直线和欧几里得空间为背景，既保持了严格的数学逻辑，又兼顾了直观性。尽管在教材初版时，形式化验证工具如Coq和Agda已经存在，但陶哲轩并未特别关注这一领域。然而，随着对形式化验证的深入了解，他意识到《Analysis I》的内容非常适合用于证明助手工具，尤其是Lean。
Lean是一种相对年轻的编程语言和证明助手，陶哲轩决定将其与《Analysis I》结合，推出了Lean版本的配套项目。该项目不仅将书中的内容转化为Lean代码，还允许读者通过填写代码中的占位符来完成证明。目前，教材中的部分内容已被翻译成Lean，并计划逐步过渡到Lean的标准数学库Mathlib。
在形式化过程中，陶哲轩有意识地在某些地方脱离Mathlib的标准定义，而在其他地方又依赖于它。例如，他在第2章中构建了不依赖于Mathlib的自然数理论，并建立了许多关于这个版本自然数的基本性质。随后，他通过练习要求读者建立这两个版本自然数之间的同构关系，并在后续章节中转而使用Mathlib中的自然数。这种模式使得项目既保持了部分自包含性，又与Mathlib保持了良好的兼容性。
这个Lean项目不仅为实分析提供了新的学习资料，同时也成为Lean和Mathlib的入门教材。通过这种方式，陶哲轩希望未来的数学本科生能够告别传统的纸笔推演，不仅计算依赖计算机，证明过程也能通过电脑完成。这一创新不仅改变了数学学习的方式，也为形式化验证在数学教育中的应用开辟了新的可能性。
原文和模型
【原文链接】 阅读原文 [ 847字 | 4分钟 ]
【原文作者】 硅星人Pro
【摘要模型】 deepseek-v3
【摘要评分】 ★★☆☆☆
相关文章
