*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 `structure`

s and `inductive`

s 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.

(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.

(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 `inductive`

s 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.

(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.

(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.

(by Kevin Buzzard, Mohammad Pedramfar)

Not a book per se, but an interactive game where you build mathematics from `inductive`

s and `axiom`

s. 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.

(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".

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.

(by Jeremy Avigad, Marijn Heule, Wojciech Nawrocki)

Didn't read yet, but looks very good, I think I might go for this one next.

(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, but heard very good things about the former.

(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.

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.

- "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 particular

- "Natural Number Game" - start with a small game to get a taste of Lean
- "Formalizing 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 gets

- "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 solutions

- "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
- "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
- "Formalizing Mathematics" - finally, good training ground for writing proofs

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.