2Learning Resources

17 entries

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 MetaM stack.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

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