Learning Resources
There are pretty good learning resources for Lean 4. Here we connect you to both written documentation for Lean 4 and to two online communities where you can follow the leaders in the field and ask questions, often getting answers very quickly.
Help Searching Mathlib for Relevant Definitions
- Mathlib Documentation
- Loogle online. Also see the Loogle VSCode extension.
Written Documentation on Lean 4 and Related Tools and Ideas
- Lean Language Site
- Lean Documentation Overview
- Functional Programming in Lean.
- Theorem Proving in Lean 4
- Meta-Programming in Lean 4
- Mathematics in Lean
- A Glimpse of Lean
- Type Checking in Lean 4
- Some Examples in Lean4
- Kevin Buzzard's Intro
- Lean for the Curious Mathematician (2023 edition)
- Learning Resources
- The Type Theory of Lean
- Type Checking in Lean
- Hitchhikers Guide to Logical Verification
- Useful Tactics for Beginners
Books on Closely Related Concepts and Tools (mainly Coq)
- Software Foundations
- The Mechanics of Proof
- Homotopy Type Theory, Chapter 1
- Survey of Logic Symbols
- Certified Programming with Dependent Types
- Software Foundations