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

主要观点总结

陶哲轩将经典数学教材《Analysis I》翻译成Lean语言，创建一个新项目让学习者通过填写Lean代码完成数学证明。这个项目成为学习Lean Mathlib的入门教程。陶哲轩的新开源项目将教材中的定义、定理和习题转化为Lean代码，为读者提供另一种学习数学的方式。他还计划将该项目逐渐过渡到标准Lean库Mathlib。

关键观点总结

关键观点1: 陶哲轩将数学教材翻译成Lean语言

陶哲轩把他的经典数学教材《Analysis I》的内容翻译成了Lean语言，创建了一个新项目，允许学习者通过编写Lean代码来完成数学证明。

关键观点2: 项目成为学习Lean Mathlib的入门教程

这个项目不仅提供了学习数学的新途径，还作为学习Lean和Mathlib的入门教程，有助于读者了解形式化验证。

关键观点3: 陶哲轩的新项目结合了Mathlib与自定义内容

陶哲轩有意识地在其新项目中结合了Mathlib和自定义内容，在某些情况下依赖Mathlib，而在其他情况下则独立于它。通过这种方式，读者可以逐渐适应Mathlib中的定义和函数，同时掌握实分析的知识。

关键观点4: 项目的意义和影响

这个项目标志着数学教学方法的转变，可能将来数学本科生将不再仅仅依赖纸张进行计算和证明。这一变革有助于将形式化验证融入到数学教学中，提高数学教育的效率和准确性。

正文

请到「今天看啥」查看全文

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

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

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

经典教材被电脑「吃了」

2006年，陶哲轩出版了一本本科生数学分析教科书，日后成为经典之作——「Analysis I」。

初版之后，该书多次更新。目前中文版到了第3版，而英文版已更新至第4版

这本教材从分析的源头——数系的结构和集合论开始，然后引向分析基础，再进入幂级数、多元微分学和傅里叶分析，最后介绍勒贝格积分。

请到「今天看啥」查看全文