新智元
整合编辑:太平洋科技
发布于:2025-06-11 15:47
陶哲轩重写20年经典教材《Analysis I》,转化为Lean编程数学证明,GitHub已发布。他借助GitHub Copilot挑战微积分ε-δ极限,形式化自己的教材并逐步过渡至标准Lean库Mathlib。通过填写Lean代码中的占位符完成证明,实现计算机辅助学习。
|
最近,陶哲轩迷上了形式化数学证明。 在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代码。
这样,读者无需再在纸上推演,而是填写Lean代码中的占位符,完成证明。 目前,书中以下部分已被翻译成Lean:
写代码,也能学数学 在形式化过程中,陶哲轩有意识地在某些地方脱离Lean的标准数学库Mathlib,而在其他地方又依赖于它。 比如,Mathlib已经定义了标准的自然数集合ℕ。 但他在第2章中构建了不依赖于Mathlib的自然数理论,并建立了许多关于这个版本自然数的基本性质,这些性质与Mathlib中ℕ的对应引理类似。 然后,在第2章结尾中,他设置了一些练习,要求读者建立这两个版本自然数之间的同构关系。 从那以后,转而使用Mathlib中的自然数。 整本书中,陶哲轩都采用这种模式—— 随着章节推进,越来越多地依赖Mathlib中的定义和函数,而不再直接引用前面章节中的自定义版本。 也就是说,他牺牲一部分「自包含性」,换取与Mathlib更好的兼容性。 因此,这个Lean项目也可以作为Lean和Mathlib的入门教材,同时也是实分析的学习资料。
部分代码片段 或许以后,数学本科生也将告别笔与纸,不仅计算要用计算机,证明也要用「电脑」。 本文来源:新智元 |
IT百科
网友评论
聚超值•精选


