陶哲轩重写20年本科经典教材！Lean编程数学证明，GitHub已放出

文章转载于新智元

最近，陶哲轩迷上了形式化数学证明。

在YouTube上，他开设了账号，上传了4段视频：如何用Lean形式化数学证明。

尤其引人注目的是第三支视频（下图右三），他借助GitHub Copilot挑战了数学分析中的基础内容——微积分中的ε-δ极限。

如今，他开始形式化自己的数学分析入门教材。

陶哲轩发布了新的开源项目，把教材中的各种定义、定理和习题翻译（或转述）为Lean语言，给学生提供另一种学习数学途径。

他还打算将新项目逐步过渡到标准Lean库Mathlib。

经典教材被电脑「吃了」

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：

写代码，也能学数学

在形式化过程中，陶哲轩有意识地在某些地方脱离Lean的标准数学库Mathlib，而在其他地方又依赖于它。

比如，Mathlib已经定义了标准的自然数集合ℕ。

但他在第2章中构建了不依赖于Mathlib的自然数理论，并建立了许多关于这个版本自然数的基本性质，这些性质与Mathlib中ℕ的对应引理类似。

然后，在第2章结尾中，他设置了一些练习，要求读者建立这两个版本自然数之间的同构关系。

从那以后，转而使用Mathlib中的自然数。

整本书中，陶哲轩都采用这种模式——

随着章节推进，越来越多地依赖Mathlib中的定义和函数，而不再直接引用前面章节中的自定义版本。

也就是说，他牺牲一部分「自包含性」，换取与Mathlib更好的兼容性。

因此，这个Lean项目也可以作为Lean和Mathlib的入门教材，同时也是实分析的学习资料。

部分代码片段

或许以后，数学本科生也将告别笔与纸，不仅计算要用计算机，证明也要用「电脑」。

点个“爱心”，再走吧