Learn Lean
Read each lesson here, then open its exercise in the editor to check your work.
Foundations
- Prove 2 + 2 = 4
Your first calculation and your first checked proof.
- Proofs are terms
Understand the Curry–Howard correspondence through an identity function.
- Values and types
Values, types, and your first expression.
- Functions
Define functions with typed parameters.
Programming
- Programs and IO
Define main and sequence IO actions with do.
- Pattern matching and recursion
Handle cases and write a recursive function.
- Lists and functions
Transform lists with anonymous functions.
Proving
- Equality proofs
Propositions, theorem, by, and rfl.
- Implication proofs
Build proofs with intro and exact.
- Proving program properties
Give an executable function a checked property.
- Mathematical symbols
Read quantifiers, logical connectives, and proof goals.
- Libraries and mathematical notation
Reuse library theorems and recognize Mathlib notation.
- Simplification with simp
Unfold a definition and simplify its arithmetic.
Cryptography
- Hashes and collisions
Use the core Hashable interface and identify its limits.
- Hash a message with SHA-256
Compute a digest of UTF-8 text without installing a package.
Advanced Lean
- Make proof checking faster
Compare two proofs of the same theorem and measure their checking times.
- Accumulators and invariants
Prove a tail-recursive loop agrees with a recursive definition.