所有Lean书籍及其寻找方法

# 所有 Lean 书籍及寻找指南 来源：https://lakesare.brick.do/all-lean-books-and-where-to-find-them-x2nYwjM3AwBQ 所有 Lean 4 教科书——印刷版，散落在地板上 尊重我目前所在城市的传统（https://www.google.com/maps/place/Underground+Printing+House+Museum/@41.6905261,44.8275181,17z/data=!3m1!4b1!4m6!3m5!1s0x40440c54b7fe64df:0xac1fe1fff2de6146!8m2!3d41.6905261!4d44.830093!16s%2Fg%2F11cs402txl?entry=ttu） *这本来可以是一个经典的“Awesome Lean”代码库（就像这个（https://github.com/sindresorhus/awesome）），但我更愿意阅读一个人对一系列书籍的主观看法，这就是你在这里会看到的。* *这些书籍没有特定顺序。* *我是并行阅读所有这些书的，我认为这是最佳方法。不过，你不应该一开始就并行阅读它们，因此我在本文的**#岔路**部分提供了一些指导。* *我还打印了大部分书籍，这帮助我把它们看作独立的书本，而不是“我在网上找到的一大坨 Lean 教程”。这也帮助我清楚地追踪读了什么没读什么。但你可能身处一个打印一本 250 页的书花费不止 4 美元的国家，所以你的体验可能有所不同。* --- ### Functional Programming In Lean [Lean 4]（https://leanprover.github.io/functional_programming_in_lean/）（作者：David Thrane Christiansen） 这是目前唯一一本将 Lean 作为普通编程语言来讲解的书。我很喜欢它。我认为它可能是函数式语言最好的入门书之一。《Functional Programming In Lean》的写作由微软赞助，你可能从《The Little Typer》听说过 David Thrane Christiansen。因此，与这份列表中的许多书不同，它是由*一位作家*撰写的。如果你不打算编写策略或用 Lean 编写程序，你可能不需要立即学习 Lean 这门语言，但我觉得不了解底层语言就不可能在 Lean 证明中感到舒适。此外，你需要理解 `structure` 和 `inductive` 才能理解 Lean 的数学对象是如何定义的。你也需要理解实例搜索才能理解 `[Group G]` 的作用。 ### Metaprogramming in Lean [Lean 4]（https://github.com/leanprover-community/lean4-metaprogramming-book）（作者：Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat） 这是关于 Lean 元编程的唯一资源。如果你不打算直接处理 Lean 内部（编写策略、参与 Lean 编译器工作、处理 lean-vscode 扩展），你可以跳过它。这本书也相当有挑战性，绝对不适合作为第一本 Lean 书籍。它假设你已经掌握了 Lean 语言，并且能够熟练编写 Lean 证明。多位作者参与了这本书的编写，我本人撰写了概述章节和练习题。书中有一种缺乏共同主线的感觉，我感觉到整体图景的缺失——我在概述章节中试图弥补这两点。这本书非常务实，理论较少，读起来像一本直奔主题的 Lean 元编程教程，学完后你应该可以开始编写策略了。 ### The Hitchhiker’s Guide to Logical Verification [Lean 3]（https://cs.brown.edu/courses/cs1951x/static_files/main.pdf）[Lean 4]（https://github.com/blanchette/logical_verification_2023/blob/main/hitchhikers_guide.pdf）（作者：Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg） 这本书读起来很愉快。在那些不是由专业作家撰写的书中，这本感觉有点像！它理论丰富，能让你在更广阔的背景下理解 Lean。书末提供了关于类型层次结构以及如何在 Lean 中定义整数/有理数/实数的最易于理解的资源之一。整本书中，你会看到类型论判断（那种中间有横线的），这表明了这本书的类型。它并非理论优先，而是理论告知。它在开头就涵盖了 Lean 中的自底向上与自顶向下证明，这个问题在我刚开始学习时确实困扰过我。我记得 Kevin Buzzard 对有人会对此感到困惑感到不解（顺便说一句——他们有充分的理由困惑！Lean 没有将多个假设合并为一个假设的策略，而这个约定并非必需，它完全可以编写这样一个策略！正是 Lean 中这类策略的缺失违背了人们的直觉），所以我很高兴《The Hitchhiker’s Guide to Logical Verification》将这个问题视为足够普遍的困惑并花时间讨论。 ### Theorem Proving in Lean [Lean 3]（https://leanprover.github.io/theorem_proving_in_lean/introduction.html）[Lean 4]（https://leanprover.github.io/theorem_proving_in_lean4/）（作者：Jeremy Avigad, Leonardo de Moura, Soonho Kong 和 Sebastian Ullrich） 和《The Hitchhiker’s Guide to Logical Verification》一样，这本书理论性很强。它细节丰富，即使你已经接触 Lean 很久，也可能会学到新东西。它全面、循序渐进，从基础开始，带你从证明项（例如 `And.intro (And.right h) (And.left h)`）到策略证明。它还有我见过的最好的关于 `inductive` 及其关联递归器的讲解，你会确切理解 Lean 基于“带归纳类型的构造演算”意味着什么。这本书由编写 Lean 的人所写，这一点显而易见。在**#岔路**部分，我建议了学习 Lean 的可能路径，而《Theorem Proving in Lean》是每条路径中唯一重复的书。 ### Mathematics in Lean [Lean 3]（https://leanprover-community.github.io/mathematics_in_lean3/）[Lean 4]（https://leanprover-community.github.io/mathematics_in_lean/）（作者：Jeremy Avigad, Patrick Massot） 《Mathematics in Lean》教你编写实际的、Mathlib 风格的证明，并定义实际的、Mathlib 风格的数学。它非常注重实践，与其说是一本书，不如说是一系列需要证明的定理。它确实从基础开始，但节奏会相当快。对于将新数学形式化到 Mathlib 中来说，这是必不可少的。 ### Logic and Proof [Lean 3]（http://leanprover.github.io/logic_and_proof_lean3/）[Lean 4]（https://leanprover-community.github.io/logic_and_proof/）（作者：Jeremy Avigad, Robert Y. Lewis, Floris van Doorn） 作为逻辑学和一般本科数学的教科书，这本书非常好。这本教科书交替出现数学章节和该数学在 Lean 中的章节，例如“关系”章节之后是“Lean 中的关系”章节。如果你确实学过数学本科，你可能会想跳过它，但对我来说，重温已知的知识很棒，这次还暗示了该数学的 Lean 实现。 ### Natural Number Game [Lean 3]（https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/）[Lean 4]（https://adam.math.hhu.de/#/g/hhu-adam/NNG4）（作者：Kevin Buzzard, Mohammad Pedramfar） 严格来说不是一本书，而是一个交互式游戏，你通过 `inductive` 和 `axiom` 来构建数学。非常有趣，不管你对证明助手的经验水平如何，都值得一试。而且它是使用证明助手的一个绝佳起点。我还没有尝试过 Lean 4 版本，它看起来比 Lean 3 版本更有吸引力。 ### Formalising Mathematics [Lean 3]（https://github.com/ImperialCollegeLondon/formalising-mathematics）[Lean 4]（https://github.com/ImperialCollegeLondon/formalising-mathematics-2024）（作者：Kevin Buzzard） 这是那种“已证明定理的宝库”类书籍，更像是一个 GitHub 仓库而非一本书。Kevin Buzzard 创建这本书是为了在伦敦帝国理工学院向博士生教授“形式化数学”课程。和《Natural Number Game》一样，Kevin Buzzard 从基础开始逐步构建数学——可以看作是《Natural Number Game》的延伸，只不过这次你直接在 vscode 中操作，数学内容也更高级。从难度上，从最简单到最难，顺序是：《Natural Number Game》，然后是《Formalising Mathematics》，最后是《Mathematics in Lean》。 ### Lean language manual [Lean 3]（https://leanprover.github.io/reference/）[Lean 4]（https://leanprover.github.io/lean4/doc/print.html） Lean 3 语言手册可以当作一本书来读。如果你不介意过时的 Lean 版本，Lean 3 版本是高质量的读物，但你在《Theorem Proving in Lean》中能找到其中的大部分内容，所以我建议直接转向那本书。Lean 4 版本不能当作书来读，而且内容与 Lean 3 版本不同，可能只是因为它是原始的、未完成的。但它确实有一些独特的内容，例如关于 User Widgets 的教程（https://leanprover.github.io/lean4/doc/examples/widgets.lean.html）——但你可以通过谷歌找到它，没必要刻意以书的形式阅读。 ### Logic and Mechanized Reasoning [Lean 4]（https://avigad.github.io/lamr/index.html）（作者：Jeremy Avigad, Marijn Heule, Wojciech Nawrocki） 这本书很棒——我最近才读完，真希望自己更早读到它，它为我奠定了逻辑学的基础。把它看作一本逻辑学教科书（命题逻辑、一阶逻辑、SAT 求解器、SMT 求解器），只不过你是在 Lean 中从零开始实现一切。所以，如果你想学习基础的逻辑学硕士课程，同时练习 Lean 作为一门普通编程语言，那就读它吧。请注意，这不是一本教你编写策略或证明定理的教科书。语言非常清晰，写作引人入胜。 --- 接下来是我没有读过的书。 ### How To Prove It With Lean [Lean 4]（https://djvelleman.github.io/HTPIwL/）（作者：Daniel Velleman） 一本刚刚宣布的书，作者是 1994 年著名教科书《How to Prove It: A Structured Approach》的作者。我两本都没读过，但听说过关于 1994 年那本的好评。 ### The Mechanics of Proof [Lean 4]（https://hrmacbeth.github.io/math2001/index.html）（作者：Heather Macbeth） Heather Macbeth 的书，配合她在福特汉姆大学的“Math 2001”课程。感谢 Fiona Skerman 推荐这本——因为我没读过，我会引用她的评论：“我真的很喜欢这本——特别是对于已经掌握大量数学但刚接触形式化证明的人来说。” ### Lean 4 tactic writing tutorial [Lean 4]（https://www.vladasedlacek.cz/en/posts/lean-01-intro）（作者：Vladimír Sedláček） 没读过，应该是《Metaprogramming in Lean》的好伴侣。无论这些博文内容如何，Lean 中的元编程资源如此稀缺，我相信你会发现这本很有帮助。 ## 岔路 就像我在介绍中提到的，我并行阅读了上述所有书。但我并没有同时*开始*它们——我是在读一本，一旦发现缺少某些上下文，就切换到另一本。所以这里我列出了我认为好的“开始阅读”顺序，这样你就不需要像我一样频繁切换了。 #### 你了解证明助手，只是刚接触 Lean 1. 《Mathematics in Lean》——克隆他们的仓库，编写 Lean 证明，你应该没问题 2. 《Theorem Proving in Lean》——深入探究 Lean 本身 #### 你只是想形式化数学 1. 《Natural Number Game》——从小游戏开始，体验 Lean 2. 《Formalising Mathematics》——继续玩游戏 3. 《Theorem Proving in Lean》——无论如何都要熟悉 Lean，你需要知道 `structure` 和 `inductive` 究竟是什么才能继续 4. 《Mathematics in Lean》——继续玩游戏，这次尽量接近 Mathlib #### 你只是想创建自己的策略 1. 《Functional Programming In Lean》——Lean 语言基础，如果你之前没用过纯函数式语言，这点尤其重要 2. 《Theorem Proving in Lean》——深入理解 Lean 作为一门语言，这里你会接触到元变量和具体化 3. 《Metaprogramming in Lean》——基本上是编写策略的教程，包含练习和解答 #### 你一无所知，从零开始 1. 《Natural Number Game》——从小游戏开始，体验 Lean 2. 《Functional Programming In Lean》——Lean 作为普通编程语言的基础 3. 《Theorem Proving in Lean》——带你从“证明项”到“策略”，两者都理解才能对 Lean 有良好感觉 4. 《Logic and Mechanized Reasoning》、《The Hitchhiker’s Guide to Logical Verification》、《Logic and Proof》——可以同时阅读，这些理论丰富、愉快的书，穿插一些 Lean 内容 5. 《Formalising Mathematics》——最后，这是编写证明的良好训练场 ## 备注 我在这里描述了我能找到的所有 Lean 书籍。如果你有更多，请告诉我。甚至长篇博文也行。 --- 用一堆纸标记的是那些：1）基于 Lean 4，并且 2）附有包含数十个已证明定理的 GitHub 仓库的书，这意味着你应该使用 Paperproof（https://github.com/Paper-Proof/paperproof）来阅读它们。 没有比看到策略/定理以动画形式影响目标和假设、以独特的物理方式呈现更好的方法来获得直观理解了。