2Learning Resources
17 entries
Books & Guides
- Functional Programming in LeanThe standard introduction to Lean as a programming language.
- Theorem Proving in Lean 4Dependent type theory and proofs in Lean.
- The Lean Language ReferenceThe official reference manual.
- Metaprogramming in Lean 4Book on macros, elaborators, tactics and the
MetaMstack.leanprover-community/lean4-metaprogramming-book - From Zero to QEDInformal introduction to Lean 4 for programmers.sdiehl/zero-to-qed
- Lean by ExampleLean and its main libraries explained through code examples (Japanese).lean-ja/lean-by-example
- Lean (meta-)programming CookbookRecipes for common programming and metaprogramming tasks.
- Tactic Programming GuideBeginner's guide to writing tactics.mirefek/lean-tactic-programming-guide
- Lean Symbol ReferenceSearchable list of Unicode symbols and their input abbreviations.
- Lean SnippetsFunctional programming patterns in Lean 4, from lazy evaluation and continuations to category-theory-inspired techniques.palladin/lean-snippets
Programming Languages & Verification
- Software Foundations in LeanThe Software Foundations textbooks, being translated from Rocq to Lean.plclub/sf-in-lean
- Programming Language Foundations in LeanLearn Lean 4 with PLFA.rami3l/PLFaLean
- Essentials of Compilation in LeanAn incremental compiler following "Essentials of Compilation".keilambda/eocia-lean
- CPDT in LeanLean implementations of material from "Certified Programming with Dependent Types".hargoniX/cpdt-lean
- Aeneas TutorialVerifying Rust programs in Lean with Aeneas (ICFP tutorial).AeneasVerif/icfp-tutorial
- Human-eval-leanHand-written, verified Lean solutions to the HumanEval benchmark, useful as idiomatic examples.leanprover/human-eval-lean
Practice
- leetproof.orgPractice platform with Lean challenges and community solutions.