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

| 机器之心报道 | | --- | 编辑：陈陈、杜伟 不得不感慨，陶哲轩真闲不住啊！ 虽然在本书撰写时，Coq 或 Agda 等一些证明助手已经相当成熟，但形式化验证当时还不在陶哲轩的考虑范围内。随着现在具备了一些这方面的经验，他意识到这 本书的内容实际上与这些证明助手非常兼容；特别地，之前用来构建标准数系等的「朴素类型理论」，与 Lean 的依赖类型理论（其中 Lean 对商类型的支持非常 出色）非常契合。 因此，陶哲轩决定创建《Analysis I》的 Lean 配套项目，将书中的许多定义、定理和练习转换成 Lean 版本。特别地，它提供一种完成书中练习的替代方法，只需 在 Lean 代码中填写对应的「待完成」（sorries）部分即可。 不过，陶哲轩不打算提供本书练习的「官方」答案。相反，他欢迎所有人自由创建这个项目的副本，并完成答题。 今天，陶哲轩又宣布 为自己的实分析本科教材《Analysis I》创建了一个「Lean」配套项目，将教材中的各种定义、定理和练习转换成 Lean 版本，为学生提供了 另一种学习方式 。Lean 既是一个交互式定理证明器，也是一种编写形式化证明的语言，近些年来在数学家群 ...