- URL: https://lean-lang.org/functional_programming_in_lean/
- License: CC BY 4.0
- Audience: Programmers new to functional programming
- Focus: Learn Lean as a programming language
- URL: https://lean-lang.org/theorem_proving_in_lean4/
- License: Apache-2.0
- Audience: Those interested in formal proofs
- Focus: Dependent type theory, proof tactics
- URL: https://leanprover-community.github.io/mathematics_in_lean/
- License: Apache-2.0
- Audience: Mathematicians
- Focus: Mathlib library, formal mathematics
- URL: https://leanprover-community.github.io/logic_and_proof/
- License: Apache-2.0
- Audience: Logic beginners
- Focus: Classical logic fundamentals
- URL: https://leanprover-community.github.io/lean4-metaprogramming-book/
- License: Apache-2.0
- Audience: Advanced users
- Focus: Writing tactics, macros, elaborators
URL: https://adam.math.hhu.de/
Available games:
- Natural Number Game (NNG4) - Prove 2+2=4 and beyond (Terence Tao endorsed!)
- Set Theory Game
- Logic Game
- Robo - A story about undergrad mathematics
- Complex Number Game
Play NNG4: https://adam.math.hhu.de/#/g/leanprover-community/NNG4
- URL: https://github.com/PatrickMassot/GlsimpseOfLean
- License: Apache-2.0
- Duration: 2-3 hours
- Author: Patrick Massot (Orsay)
- Focus: Fast-paced interactive introduction
- URL: https://github.com/leanprover-community/tutorials4
- License: Apache-2.0
- Origin: Orsay Lean course
- Focus: Practical exercises with solutions
- URL: https://github.com/PatrickMassot/verbose-lean4
- License: Apache-2.0
- Feature: Natural language tactics
- Languages: French and English
- Use: Teaching beginners with readable proof language
- URL: https://github.com/jaalonso/An_introduction_to_Lean_4
- License: GPL-2.0
- Level: Beginner
- Edition: September 2025
- Author: Heather Macbeth
- URL: https://hrmacbeth.github.io/math2001/
- Level: Early university
- Focus: Mathematical proof techniques
- Author: Kevin Buzzard
- URL: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024
- License: Apache-2.0
- Bonus: YouTube lecture videos available
| Event | Location | Dates |
|---|---|---|
| MPS Workshop on Lean | New York | June 16-20, 2025 |
| Summer School Formalizing Math | Utrecht | July 21-25, 2025 |
| Formalizing Class Field Theory | Oxford | July 21-25, 2025 |
| Lean Together 2026 | Virtual | Jan 19-23, 2026 |
- URL: https://emallson.net/blog/a-beginners-companion-to-theorem-proving-in-lean/
- Focus: Supplements official TPIL book
- URL: https://brandonrozek.com/blog/lean4-tutorial/
- Focus: Getting started quickly
- URL: https://jessealama.net/getting-started-with-lean-4/
- Focus: First steps
- URL: https://unreasonableeffectiveness.com/learning-lean-4-as-a-programming-language-project-euler/
- Focus: Lean as a programming language
- URL: https://learnxinyminutes.com/lean4/
- Compact syntax overview
- PDF available from leanprover-community
- Common tactics reference
Install the lean4 extension from marketplace.
- Repository: https://github.com/leanprover-community/lean4-mode
- Requires: Emacs 27+, lsp-mode, dash, magit-section
;; Doom Emacs
;; In packages.el:
(package! lean4-mode
:recipe (:host github
:repo "leanprover-community/lean4-mode"
:files ("*.el" "data")))
;; Standard use-package with straight.el
(use-package lean4-mode
:commands lean4-mode
:straight (lean4-mode
:type git
:host github
:repo "leanprover-community/lean4-mode"
:files ("*.el" "data")))Key bindings:
C-c C-i: Toggle info view (proof state)
- URL: https://leanprover.zulipchat.com/
- Active 24/7, welcoming community
- Topic-based organization
- Best place for questions
- Lean 4 Anarchy: https://discord.gg/WZ9bs9UCvx
- Functional Programming Discord: #lean channel
- Lean 4: https://github.com/leanprover/lean4
- Mathlib: https://github.com/leanprover-community/mathlib4
- Community: https://github.com/leanprover-community
- Formalising Mathematics 2022 playlist on YouTube
- Imperial College London lectures
- Conference recordings (Lean Together 2021-2026)
- Tutorial videos
- 2021 video tutorial available
- URL: HuggingFace datasets
- Content: 57K autoformalized problems
- Focus: High-school contest math, IMO problems
- Accuracy: 93.5%
- URL: https://arxiv.org/abs/2512.18160
- Authors: Wilf, Aggarwal, Parno, Fried, et al.
- Focus: Self-play training via formal verification
- Tool: Verus (Rust verification)
- Result: 9.6x improvement in code generation
- Relevance: Shows verification as training oracle
- Level: Graduate CS/PL theory
- Note: Copyright (All Rights Reserved) - reference only
gmake deps # Check your tools- URL: https://github.com/leanprover/elan
- Like rustup for Lean
- Recommended for managing multiple versions
- Day 1: Play Natural Number Game
- Day 2: Read FPIL chapters 1-3
- Day 3: Try Glimpse of Lean (2-3 hours)
- Week 1: Complete this workshop’s exercises
- Week 2+: Choose path:
- Programming → Continue FPIL
- Proofs → Read TPIL
- Mathematics → Start MIL
- Natural Number Game completion
- Implement and prove basic list operations
- Formalize a small mathematical structure
- Add to the satirical examples collection
- Create a domain-specific example (crypto, security)