标签：Lean
陶哲轩重写20年本科经典教材！Lean编程数学证明，GitHub已放出
陶哲轩最近对形式化数学证明产生了浓厚兴趣，并在YouTube上开设了账号，上传了四段视频，专门介绍如何使用Lean进行形式化数学证明。其中，第三支视频尤为引人...
陶哲轩：感谢Lean，我又重写了20年前经典教材！
陶哲轩近日宣布为其本科教材《Analysis I》创建了一个Lean配套项目，将书中的定义、定理和练习转换为Lean版本，为学生提供了一种新的学习方式。Lean是一种交...
