所有精益书籍以及在哪里可以找到它们

所有精益书籍以及在哪里可以找到它们尊重我目前所在城市的传统这可能是一个经典的“很棒的精益”存储库（就像这样），但是我更喜欢阅读单个人对一系列书籍的主观意见，这就是您将在这里看到的。这些书不按任何顺序呈现。我并行阅读了所有这些内容，我认为这是最好的方法。然而，您不应该同时“启动”所有这些，因此我在本文的#Forking paths 部分提供了一些指导。我还印刷了大部分这些书，我认为这帮助我将它们视为单独的书，而不是“我在网上找到的精益教程的一个整体”。它帮助我正确地记录我读过的内容和未读过的内容。但在您所在的国家/地区，打印一本 250 页的书的成本可能不是 4 美元，因此您的情况可能会有所不同。精益中的函数式编程 [Lean 4]（作者：David Thrane Christiansen）这是目前唯一一本将精益作为普通编程语言进行介绍的书籍。我喜欢它。我认为这可能是对函数式语言最好的介绍之一。 《精益函数式编程》的写作是由微软赞助的，你可能在他的《小打字机》中听说过 David Thrane Christiansen。因此，与此列表中的许多书籍不同，它是由作家撰写的。如果您不打算编写策略/使用精益来编写代码，也许您并不立即需要学习精益作为一种语言，但我无法想象在不了解底层语言的情况下编写精益证明会感到舒服。此外，你确实需要理解结构和归纳来理解精益的数学对象是如何定义的。而且您确实需要了解实例搜索才能了解 [Group G] 正在做什么。精益元编程 [Lean 4]（作者：Arthur Paulino、Damiano Testa、Edward Ayers、Evgenia Karunus、Henrik Böving、Jannis Limperg、Siddhartha Gadgil、Siddharth Bhat）这是有关精益元编程的唯一资源。如果使用精益内部原理（编写策略、使用精益编译器、使用精益 vscode 扩展）不在您的直接计划中，您可以跳过它。它也相当具有挑战性，它当然不应该被用作第一本精益书籍。它假设您了解精益作为一种语言，并且假设您能够轻松编写精益证明。许多作者都为本书做出了贡献，我自己编写了概述章节和练习。有一种缺少共同线索的感觉，而且我觉得缺少更大的图景——相应地，我试图在概述一章中弥补这两点。它非常有根据，几乎没有什么理论，读起来就像是关于精益元编程的开门见山的教程，读完之后你应该准备好开始编写策略了。逻辑验证搭便车指南 [精益 3] [精益 4]（作者：Anne Baanen、Alexander Bentkamp、Jasmin Blanchette、Johannes Hölzl、Jannis Limperg）读起来很愉快。在所有非作家写的书中，这本书感觉有点像作家写的！它的理论很丰富，应该让您在更广泛的背景下了解精益。书的末尾有关于类型层次结构以及如何在精益中定义整数/有理数/实数的最容易访问的资源之一。在整本书中，你会看到类型理论的判断（中间有一条水平线），这应该作为这本书的一个例子。它不是理论优先，但它是基于理论的。它从一开始就涵盖了精益中自下而上与自上而下的证明，这个话题在我刚开始时确实困扰着我。我记得凯文·巴扎德（Kevin Buzzard）很困惑为什么有人会对此感到困惑（顺便说一句 - 他们感到困惑是有充分理由的！精益没有将多个假设统一为一个假设的策略，而且这个约定不必成立，完全有可能编写一个策略来做到这一点！精益中缺乏这样的策略，这违背了人们的直觉），所以我很高兴“逻辑验证搭便车指南”认为这是一个普遍存在的困惑，值得花一些时间来研究它。精益中的定理证明 [精益 3] [精益 4]（作者：Jeremy Avigad、Leonardo de Moura、Soonho Kong 和 Sebastian Ullrich）就像《逻辑验证漫游指南》一样，它充满了理论。它充满了细节，即使您已经使用精益很长时间，您也可能会学到一些新东西。它是彻底的、渐进的，从头开始，带你从证明术语（例如 And.intro (And.right h) (And.left h) ）到策略证明。它还有我所见过的对归纳及其相关递归器的最好解释，您将确切地理解基于“归纳类型的构造演算”对精益意味着什么。它是由那些写过《精益》的人写的，它表明了这一点。在#Forking paths 部分，我建议了学习精益的可能路径，《精益定理证明》是唯一的书