All Lean Books and Where to Find Them

This article provides a subjective guide to key Lean programming books, including "Functional Programming in Lean" for learning Lean as a language, "Metaprogramming in Lean" for advanced work with Lean internals, and "The Hitchhiker's Guide to Logical Verification" for understanding Lean within a broader theoretical context. The author recommends reading multiple books in parallel rather than sequentially, and suggests that understanding Lean as a programming language is essential for writing proofs and working with Lean's mathematical structures.