陶哲轩宣布为自己的实分析本科教材《Analysis I》创建了一个「Lean」配套项目，将教材中的定义、定理和练习转换成 Lean 版本，旨在为学生提供另一种学习方式，并逐步过渡到标准的 Lean 库 Mathlib。
该项目不仅作为实分析的辅助教材，还能作为 Lean 与 Mathlib 的入门指南，鼓励数学系学生、Lean 初学者及对形式化验证感兴趣的科研人员参与挑战。
网友对此表示非常兴奋，认为这将提供即时反馈，帮助学生更有效地学习数学，并期待未来能够获得更多更具指导性的反馈。
陶哲轩宣布为自己的实分析本科教材《Analysis I》创建了一个「Lean」配套项目，将教材中的定义、定理和练习转换成 Lean 版本，旨在为学生提供另一种学习方式，并逐步过渡到标准的 Lean 库 Mathlib。
该项目不仅作为实分析的辅助教材，还能作为 Lean 与 Mathlib 的入门指南，鼓励数学系学生、Lean 初学者及对形式化验证感兴趣的科研人员参与挑战。
网友对此表示非常兴奋，认为这将提供即时反馈，帮助学生更有效地学习数学，并期待未来能够获得更多更具指导性的反馈。
