Learning Lean: Part 1
13 days ago
- #formal mathematics
- #dependent types
- #Lean theorem prover
- 作者受到用Lean普及数学形式化运动的启发，强调其优势如错误检测和减少合作者间的信任需求。
- 形式化让数学家能专注于写作中的直觉与动机，而非细节的机械验证，这在大语言模型(LLM)时代尤为珍贵。
- 作者展望数学家与AI的未来协作：AI协助高层证明策略，Lean处理形式化证明，最终论文聚焦证明的'故事性'。
- 作者分享背景：数学博士（代数/数论/组合数学方向），后转型为软件工程师（主攻Web前端开发）。
- 作者探讨学习Lean的挑战，尤其是需要理解类型论和逻辑学等数学家较少接触的基础理论。
- 作者将学习Lean比作研读外语经典文本，需同时掌握多个深奥且独立的知识体系。
- 作者完成了《自然数游戏》和《集合游戏》在线教程，认为这是很好的Lean入门方式。
- 作者解析Lean的三层结构：项(terms)、类型(types)和宇宙(universe)，及其交互关系的理解难点。
- 作者指出Lean因类型与项世界的混合而导致的语法混淆，与TypeScript等语言的明确区分形成对比。
- 作者讨论Lean中可选的命名与类型标注机制，这对初学者可能造成困惑。
- 作者分享初期在数字字面量和类型类(type class)上的困惑，联想到早年学习Haskell的类似经历。
- 作者反思Lean中Prop与Type宇宙分离等理论设计与实际应用的差异。
- 作者列出关于Lean的未解疑问：定义等价性、Prop与Decidable的区别、#eval与#reduce的差异等。
- 作者惊叹于Lean仅用少量基础构造就能构建整个已知数学体系的能力。
- 作者感谢Lean Zulip社区的帮助，提到用Claude解答简单问题，复杂问题仍需专家指导。