This 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.
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
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.
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 all 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.
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.
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" 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.
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.
Not a book per se, but an interactive game where you build mathematics from
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.
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".
It's good, and the only reason why you might want to avoid it is it's only available in Lean 3 at the moment, I do hope they port it soon.
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.
Didn't read yet, but looks very good, I think I might go for this one next.
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, but heard very good things about the former.
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.
Like 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 I was understanding I'm missing some context.
So here I lay out what I think might be a good "starting to read" order might be, so that you don't need to switch as frequently as I did.
inductiveexactly is to proceed
I 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, and
2) 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 intuition for what a particular tactic is doing than to see it as an animation that affects your goals and hypotheses in a distinct physical way.