主要观点：作者被 Lean 定理证明器推动的数学形式化运动吸引，深入学习 Lean 并分享个人学习笔记。形式化有诸多好处，如捕捉证明错误等，还能更好地分离数学写作中的关注点，对大型语言模型时代的数学写作有重要意义，未来数学家可与 AI 合作。
关键信息：

• 推荐观看 Kevin Buzzard 关于形式化数学的 YouTube 演讲。
• 形式化能让数学家专注于人类理解的关键，而不是机械验证细节。
• 作者背景包括博士毕业于数学专业，做过一年博士后未成为研究数学家，对编程语言有兴趣等。
• 学习 Lean 语言过程中遇到三层次对象、语法分离、可选名与可选类型、数字字面量与类型类等问题。
• 体会到 Curry-Howard 理论中程序和证明虽理论上相同但实践中仍有区别。
  重要细节：
• Lean 有术语、类型、宇宙三层类型层次，类型可作为其他类型的类型。
• 在依赖类型语言中，语法上区分“类型世界”和“值世界”较难，初学者易迷失。
• 变量名可添加到类型签名中，导致新手混淆。
• 数字字面量是类型类对象，新手易在此处出错。
• 对 Lean 中一些概念如 Prop 与 Decidable、#eval 与 #reduce 等仍有疑问。
• 作者认为 Lean 基于少量基础构建了庞大的数学体系，学习资料有优点也有不足，准备继续学习数学在 Lean 中的应用，感谢 Lean Zulip 社区的帮助。