GoKawiilRespecting traditions of the city I'm currently in
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.
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 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.
Metaprogramming in Lean [Lean 4]
... continue reading