陶哲轩：感谢Lean，我又重写了20年前经典教材！

数学家陶哲轩为其实分析教材《Analysis I》创建了Lean配套项目，将书中内容形式化为Lean代码，为学生提供新学习方式。Lean作为交互式定理证明器正受数学界欢迎，项目计划逐步融入Mathlib。尽管部分章节未优化且习题以占位符呈现，但陶哲轩鼓励读者自由参与完善。此项目既是辅助教材，也是Lean入门指南，受到网友好评并引发对更智能反馈机制的期待。
来源：https://mp.weixin.qq.com/s/VE3bnSVRnNWnTDVMme45Sw