← #795

学 Lean 定理证明器，该读哪些书：一份私人书单

查看原文 HN 讨论

文章摘要

这份清单容易让人误会——它与「精益创业」或「精益生产」毫无关系，而是关于 Lean 4：一种用于形式化数学与定理证明的证明助手（proof assistant）兼函数式编程语言的学习资源指南。作者 Evgenia Karunus 明确说，她不想再做一个冷冰冰的「awesome-list」式仓库，而「更愿意读到某一个人对一整批书的主观看法」。

她已读过并点评的书包括：《Functional Programming in Lean》（编程基础，建议作为前置）、《Metaprogramming in Lean》（进阶的策略 tactic 编写，需有 Lean 基础）、《The Hitchhiker’s Guide to Logical Verification》（理论扎实但讲解平易）、《Theorem Proving in Lean》（综合性参考书，几乎出现在每条推荐学习路径里）、《Mathematics in Lean》（贴近 Mathlib 风格的实战证明）、《Logic and Proof》、《Natural Number Game》（互动游戏，推荐作为起点）、《Formalising Mathematics》（GitHub 仓库）、《Lean Language Manual》以及《Logic and Mechanized Reasoning》。她也列出了尚未读、仅作提及的几本，如《How To Prove It With Lean》《The Mechanics of Proof》《Lean 4 Tactic Writing Tutorial》。

清单的组织方式很实用：按读者背景提供了四条「分岔路径（Forking Paths）」——已有证明助手经验的人、专注数学形式化的人、想做策略开发的人、以及完全的新手——分别给出不同的阅读顺序。作者在每本书旁附上主观评价，包括写作质量、上下文缺口和教学效果，并提到把书打印出来有助于记忆、也帮助她在概念上区分不同资源。

HN 评论精华

这是个相对冷门、讨论不多的帖子，主要的两条评论都聚焦在「Lean 是什么」以及它的学习曲线上。

• ptrott2017：感谢发帖人——他看到标题时也以为是关于精益创业或精益生产的书，「非常高兴发现这其实是一批关于 Lean 编程语言的书的链接集合，而且网站其余部分也很值得一读，这让我一早上心情都好了！」
• mattgoupil：好帖，但它也从侧面说明「一旦深入，Lean 是一张多么错综复杂的网」。他指出，你当然可以只把 Lean 当普通编程语言来用，但那就太可惜了——证明（proof）是 Lean 整个世界观里固有的一部分，而证明会把你带入一个少有程序员体验过的视角。他进而设想：Lean 或许需要一种超文本式的教程，让路径随读者的需求展开、能够回退再走另一条路，而不必同时在一堆分开的标签页里开着这么多本书。