All Lean Books And Where To Find Them

Evgenia Karunus
/All Lean Books And Where To Find ThemAll Lean Books And Where To Find ThemRespecting 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.These books are not presented in any order.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.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.Functional Programming In Lean [Lean 4] (by David Thrane Christiansen) 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.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.Metaprogramming in Lean [Lean 4](by Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil, Siddharth Bhat) 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.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.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.The Hitchhiker’s Guide to Logical Verification [Lean 3] [Lean 4]  (by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg)This one was a pleasure to read.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.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. Theorem Proving in Lean [Lean 3] [Lean 4] (by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich)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".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 Proving in Lean" is the only book that repeats in every path.Mathematics in Lean [Lean 3] [Lean 4]  (by Jeremy Avigad, Patrick Massot)"Mathematics in Lean" teaches you to write actual, Mathlib-style proofs, and define actual, Mathlib-style mathematics. It's very hands-on, it's less of a book and more of a series of theorems to prove. It does take you from the ground up, however the pace will be quite fast.Indispensable for formalizing new mathematics for Mathlib.Logic and Proof [Lean 3] [Lean 4](by Jeremy Avigad, Robert Y. Lewis, Floris van Doorn)This was very good as a textbook on logic, and undergrad mathematics in general. This textbook alternates chapters on mathematics with chapters on that mathematics in Lean, for example chapter "Relations" is followed by the chapter "Relations in Lean".You might want to miss out on it if you have actually done a mathy bachelor, but for me it was great to repeat what I knew already, this time with suggestive winks towards Lean implementations of said mathematics.Natural Number Game [Lean 3] [Lean 4] (by Kevin Buzzard, Mohammad Pedramfar)Not a book per se, but an interactive game where you build mathematics from inductives and axioms. Supremely fun, do try it out, whatever your experience level with proof assistants is.And it's a perfect start as a first step in proof assistants.I haven't tried the Lean 4 version yet, it looks even more appealing than the Lean 3 version.Formalising Mathematics [Lean 3] [Lean 4] (by Kevin Buzzard)This is one of those "treasure trove of proved theorems" kind of books, more of a github repo than a book. Kevin Buzzard created this book to teach the "Formalising mathematics" course to PhD students at Imperial College London.As in the "Natural Number Game", Kevin Buzzard builds up mathematics from the ground up - consider it an extension of the "Natural Number Game", except this time you do it directly in vscode & the maths is getting more advanced.In terms of difficulty, from the simplest to the hardest, it would be: "Natural Number Game", then "Formalising Mathematics", and then "Mathematics in Lean".Lean language manual [Lean 3] [Lean 4]The Lean 3 language manual could  be read as a book. The Lean 3 version is a quality read if you're not intimidated by the stale Lean version, however most of what you'll find there can found in "Theorem Proving in Lean", so I'd just switch directly to that one.The Lean 4 version cannot be read as a book, and in general has contents that differ from the Lean 3 version, probably just because it's raw and unfinished. It does have some unique contents however, e.g. a tutorial on User Widgets - but you can find that via google, there is no need to purposefully read it in the form of the book.Logic and Mechanized Reasoning [Lean 4](by Jeremy Avigad, Marijn Heule, Wojciech Nawrocki)This book was great - I read it very recently, and I do wish I read it earlier, it grounded logic for me.Consider this a textbook on logic (Propositional/First-Order Logics,  SAT solvers, SMT solvers), except you are implementing everything from the ground up in Lean. So, go for it if you want to learn a basic logic master's curriculum AND practice Lean as a normal programming language.Note that this is not a textbook that will teach you to write tactics or to prove theorems.The language is pefectly clear, the writing is entertaining.Next come the books I did not read.How To Prove It With Lean [Lean 4] (by Daniel Velleman)A just-announced book from the author of the famous 1994's "How to Prove It: A Structured Approach" textbook. I haven't read either of these books, but heard good things about the 1994 one.The Mechanics of Proof [Lean 4] (by Heather Macbeth)A book by Heather Macbeth, accompanying her "Math 2001" course at Fordham University.Thanks to Fiona Skerman for sending this one in - as I didn't read it myself, I will include her comment instead: "I really like this one - particularly as a way for people who know a bunch of maths but are new to formalising proofs".Lean 4 tactic writing tutorial [Lean 4](by Vladimír Sedláček)Didn't read, should be a good accompaniment to "Metaprogramming in Lean". Whatever the contents of those blog posts are, the resources on metaprogramming in Lean are so scarce I'm sure you'll find this beneficial.Forking pathsLike I mentioned in the introduction, I was reading all of the aforementioned books in parallel.I didn't start all of them in parallel, however, - I was reading one and switching to another one as soon as it was clear to me I'm missing some context.So here I lay out what I think a good "starting to read" order might be, so that you don't need to switch as frequently as I did.You know proof assistants, you're just new to Lean"Mathematics in Lean" - just clone their repo and write Lean proofs, you should be good"Theorem Proving in Lean" - for a deeper dive into Lean in particularYou just want to formalize mathematics"Natural Number Game" - start with a small game to get a taste of Lean"Formalising Mathematics" - continue with playing the game"Theorem Proving in Lean" - familiarise yourself with Lean either way, you'll want to know what a structure and inductive exactly is to proceed"Mathematics in Lean" - continue with playing the game, this time as close to Mathlib as it getYou just want to create your own tactics"Functional Programming In Lean" - basics of the Lean language, especially important if it's your first purely functional language"Theorem Proving in Lean" - a deeper dive into Lean as a language, here you'll get a taste for metavariables and elaboration"Metaprogramming in Lean" - basically a tutorial on tactic writing, with exercises and solutionsYou don't know anything, as from the ground up as it gets"Natural Number Game" - start with a small game to get a taste of Lean"Functional Programming In Lean" - basics of Lean as a normal programming language"Theorem Proving in Lean" - will take you from "proof terms" to "tactics", both are essential to understand to get a good feeling of Lean"Logic and Mechanized Reasoning", "The Hitchhiker’s Guide to Logical Verification", "Logic and Proof" - can be read at the same time, pleasant, theory-laden books with some Lean intermissions"Formalising Mathematics" - finally, good training ground for writing proofsNotesI described here all books on Lean I could find. Do send more my way.Even send me lengthy blog posts.Marked with a lump of paper were the books that are:1) in Lean 4, and2) come with a github repo with dozens of proved theorems,meaning you should benefit from using Paperproof with them.There is no better way to get an intuition for what a particular tactic/theorem is doing than to see it as an animation that affects your goals and hypotheses in a distinct physical way.Published with Brick

The provided text offers a curated collection of resources and a suggested approach for learning Lean, a proof assistant, emphasizing the distinction between learning Lean as a programming language and using it for formalizing mathematics. The author recommends reading these materials in parallel, while offering guidance on the optimal sequence depending on the learner's objective.

For foundational understanding of Lean as a programming language, Functional Programming In Lean is highlighted as an excellent introduction, especially beneficial for those learning functional languages, and it has received sponsorship from Microsoft. To grasp the underlying structure of Lean, understanding functional programming concepts is noted as necessary, along with an understanding of structures and inductives, which are crucial for comprehending how Lean defines its mathematical objects and instance search. For those interested in the internal workings of Lean, such as writing tactics or working on the compiler, Metaprogramming in Lean is presented as the dedicated resource, although it is acknowledged as challenging and presupposes familiarity with Lean as a language.

Regarding the theoretical and structural foundations, several books provide context. The Hitchhiker’s Guide to Logical Verification is praised for being rich in theory and placing Lean in a broader context, offering an exploration of type theory judgments and the hierarchy of types. Theorem Proving in Lean is described as thorough and theory-laden, guiding the reader gradually from proof terms to tactic proofs and offering an excellent explanation of inductives and recursors, demonstrating how Lean is based on the Calculus of Constructions with inductive types. Further theoretical grounding is provided by Logic and Proof, which alternates between mathematics and their implementations in Lean, and Logic and Mechanized Reasoning, which grounds logic, proposition logic, and satisfiability solvers within the Lean framework.

The formalization of mathematics is addressed through several hands-on approaches. Mathematics in Lean teaches the practical skill of writing proofs and defining mathematics in the style of Mathlib, focusing on proving theorems rather than purely theoretical exposition. This is complemented by Formalising Mathematics, which functions as an extension of interactive exercises, allowing the structured building of mathematics from the ground up, similar to the Natural Number Game. The Natural Number Game is recommended as a fun, interactive starting point for understanding proof assistants by building mathematics from inductives and axioms.

The author suggests specific learning paths. For someone new to proof assistants, starting with Formalising Mathematics and the Natural Number Game is recommended. For those who want to deepen their knowledge of Lean itself, Theorem Proving in Lean and Mathematics in Lean provide deep dives, with the latter being more focused on practical theorem proving and the former on the language's structure. If the goal is to learn to write custom tactics, Metaprogramming in Lean and the Lean 4 tactic writing tutorial are suggested. For building a holistic understanding, the author advises reading the foundational logic texts, such as The Hitchhiker’s Guide to Logical Verification, alongside the practical Lean texts. The Lean language manual is noted, though the focus should be placed on Theorem Proving in Lean for practical application. Overall, the approach balances learning the underlying logical and mathematical theory with the practical application of Lean's programming and proof system.