陶哲轩重写20年本科经典教材！Lean编程数学证明，GitHub已放出
文章转载于新智元
最近，陶哲轩迷上了形式化数学证明。
在YouTube上，他开设了账号，上传了4段视频：如何用Lean形式化数学证明。
尤其引人注目的是第三支视频（下图右三），他借助GitHub Copilot挑战了数学分析中的基础内容——微积分中的ε-δ极限。
如今，他开始形式化自己的数学分析入门教材。
陶哲轩发布了新的开源项目，把教材中的各种定义、定理和习题翻译（或转述）为Lean语言，给学生提供另一种学习数学途径。
他还打算将新项目逐步过渡到标准Lean库Mathlib。
1
经典教材被电脑「吃了」
2006年，陶哲轩出版了一本本科生数学分析教科书，日后成为经典之作——「Analysis I」。
初版之后，该书多次更新。目前中文版到了第3版，而英文版已更新至第4版
这本教材从分析的源头——数系的结构和集合论开始，然后引向分析基础，再进入幂级数、多元微分学和傅里叶分析，最后介绍勒贝格积分。
全书几乎完全是以具体的实直线和欧几里得空间为背景，保留了足够的直观性，完美结合了严格性和直观性。
当时，虽然像Coq和Agda之类的证明助手（proof assistant）已经比较成熟，但陶哲轩并没有特别关注形式化验证。
证明助手Agda第一版发布于1999年，而Coq第一版发布于1989年
近二十年后，随着对形式化验证的深入了解，陶哲轩意识到，《Analysis I》的内容非常适合用于证明助手工具。
Lean是一种更年轻的编程语言和证明助手
因此，他决定为《Analysis I》推出Lean版本的配套项目，将书中的定义、定理和练习「翻译」成Lean代码。
项目地址：https://github.com/teorth/analysis
这样，读者无需再在纸上推演，而是填写Lean代码中的占位符，完成证明。
目前，书中以下部分已被翻译成Lean：
1
写代码，也能学数学
在形式化过程中，陶哲轩有意识地在某些地方脱离Lean的标准数学库Mathlib，而在其他地方又依赖于它。
比如，Mathlib已经定义了标准的自然数集合ℕ。
但他在第2章中构建了不依赖于Mathlib的自然数理论，并建立了许多关于这个版本自然数的基本性质，这些性质与Mathlib中ℕ的对应引理类似。
然后，在第2章结尾中，他设置了一些练习，要求读者建立这两个版本自然数之间的同构关系。
从那以后，转而使用Mathlib中的自然数。
整本书中，陶哲轩都采用这种模式——
随着章节推进，越来越多地依赖Mathlib中的定义和函数，而不再直接引用前面章节中的自定义版本。
也就是说，他牺牲一部分「自包含性」，换取与Mathlib更好的兼容性。
因此，这个Lean项目也可以作为Lean和Mathlib的入门教材，同时也是实分析的学习资料。
部分代码片段
或许以后，数学本科生也将告别笔与纸，不仅计算要用计算机，证明也要用「电脑」。
