All Lean Books and Where to Find Them
4 hours ago
- #Learning Path
- #Lean Books
- #Functional Programming
- The repository offers subjective opinions on Lean books instead of a classic 'Awesome Lean' list.
- Reading multiple Lean books in parallel is recommended, but not starting all at once.
- Printing books can help separate them mentally, though cost may vary.
- 'Functional Programming In Lean' covers Lean as a normal programming language, sponsored by Microsoft.
- 'Metaprogramming in Lean' is the only Lean metaprogramming resource; it's challenging and not for beginners.
- 'The Hitchhiker’s Guide to Logical Verification' is theory-informed, covering bottom-up vs. top-down proofs.
- 'Theorem Proving in Lean' is thorough, starting from proof terms to tactics, written by Lean creators.
- 'Mathematics in Lean' teaches Mathlib-style proofs and definitions, hands-on with a fast pace.
- 'Logic and Proof' is a textbook on logic with Lean implementations, clear and entertaining.
- 'Introduction to Proofs and Proof Strategies' alternates math chapters with Lean chapters.
- 'Natural Number Game' is an interactive game building math from axioms, fun for all levels.
- 'Formalising Mathematics' builds advanced math from the ground up, like an extended Natural Number Game.
- Lean 3 manual can be read as a book, but Lean 4 version is raw and unfinished.
- 'Computational Logic' implements logic from the ground up in Lean, teaching logic curriculum.
- Unread books include 'Proof and Proving in Lean', 'Math 2001', and 'Lean Blog Posts on Metaprogramming'.
- Forking paths section suggests starting orders to avoid frequent switching between books.
- Books marked with paper lumps are Lean 4 with GitHub repos, suitable for Paperproof animations.