All Lean Books And Where To Find Them
All Lean Books And Where To Find Them<br>Respecting traditions of the city I'm currently inThis could have been a classic "Awesome Lean" repo (like this), however I'd much prefer reading subjective opinions of a single person on a whole range of books, and this is what you'll have here.<br>These books are not presented in any order.<br>I was reading all of these in parallel, and I think it's the best approach here. You shouldn't *start* all of these in parallel however, so I'm offering some guidance in the #Forking paths section of this post.<br>I also printed most of these books, I think it helped me perceive them as separate books as opposed to "a single lump of a Lean tutorial I found online". And it helped me properly keep track of what I have and haven't read. But you might be in a country where printing out a 250-page book costs something other than 4$, so your mileage may vary.<br>Functional Programming In Lean [Lean 4]<br>(by David Thrane Christiansen)<br>This is the only currently existing book that covers Lean as a normal programming language. I loved it. I think it might be one of the best introductions to functional languages altogether. The writing of "Functional Programming In Lean" was sponsored by Microsoft, you might have heard of David Thrane Christiansen from his "The Little Typer". So, unlike many of the books on this list, it was written by a writer.<br>Maybe you don't immediately need to learn Lean as a language if you don't plan to write tactics/use Lean to code something up, but I cannot imagine feeling comfortable writing Lean proofs without knowing the underlying language. Besides, you do need to understand structures and inductives to understand how Lean's mathematical objects are defined. And you do need to understand instance search to understand what [Group G] is doing.<br>Metaprogramming in Lean [Lean 4]<br>(by Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat)<br>This is the only resource on Lean metaprogramming. You can skip it if working with Lean internals (writing tactics, working on the Lean compiler, working on the lean-vscode extension) is not in your direct plans. It is also quite challenging, it certainly shouldn't be used as the first Lean book. It assumes you know Lean as a language, and it assumes you're comfortable with writing Lean proofs.<br>Many authors have contributed to this book, I myself wrote the Overview chapter and exercises. There was some sense of a missing common thread, and I felt the bigger picture was missing - both of which I, correspondingly, tried to remedy in the Overview chapter.<br>It's very grounded, has little theory, and reads as a straight to the point tutorial on Lean metaprogramming, by the end of which you should be ready to start writing tactics.<br>The Hitchhiker’s Guide to Logical Verification [Lean 3] [Lean 4]<br>(by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg)<br>This one was a pleasure to read.<br>Among the books that were not written by writers, this one feels like it sort of was! It's rich in theory, and it should let you see Lean in a wider context. End of the book has one of the most accessible resources on hierarchy of types and on how we can define integers/rationals/reals in Lean. Throughout the book, you will see type theory judgements (with a horizontal line in-between, those ones), this should serve as an example of what kind of a book this is. It's not theory-first, but it is theory-informed.<br>It covers bottom-up VS top-down proofs in Lean in the very beginning, a topic that did bother me when I was starting out. I remember Kevin Buzzard was confused why anybody is ever confused about that (by the way - they are confused for a good reason! Lean doesn't have tactics that unite multiple hypotheses into a single hypothesis, and this convention doesn't have to hold, it's perfectly possible to write a tactic that would do it! It's the absence of such tactics in Lean that goes against people's intuitions), so I'm glad "The Hitchhiker’s Guide to Logical Verification" considered that a widespread enough puzzlement to spend some time on it.<br>Theorem Proving in Lean [Lean 3] [Lean 4]<br>(by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich)<br>Like "The Hitchhiker’s Guide to Logical Verification", it's theory-laden. It's so packed with details you'll probably learn something new even if you've been around Lean for a long time. It's thorough, gradual, and starts from the ground up, taking you from proof terms (e.g. And.intro (And.right h) (And.left h)) to tactic proofs. It also has the best explanation of inductives and their associated recursors I have seen, you will understand exactly what it means for Lean to be based on "Calculus of Constructions with inductive types".<br>It was written by people who wrote Lean and it shows. In the #Forking paths section where I suggest possible paths to learning Lean, "Theorem...