A hands-on workbook

Learn Lean 4 by solving exercises

Lean is a functional programming language that is also a proof assistant. Each module has worked examples followed by exercises marked with sorry. Replace every sorry with a definition or a proof, and Lean checks your work.

Get startedJump to module 1
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  sorry  -- your turn: replace this with a proof

Modules

Go in order, and move on once a module compiles without any sorry.

Module 1

Lean as a programming language

  • Evaluate expressions with #eval and inspect types with #check.
  • Define functions with def.
  • Recursion and pattern matching (match).
0/3 solved
Module 2

Propositions and proofs

  • Understand that propositions are types and proofs are terms.
  • Use the basic tactics: intro, exact, apply, constructor, cases, rfl, rw, simp.
  • Propositional logic: →, ∧, ∨, ¬, ↔.
0/5 solved
Module 3

Induction: proving things about your programs

  • Proofs by induction on Nat and List.
  • Combine simp, rw and the induction hypothesis.
  • Verify properties of functions you wrote yourself.
0/5 solved

How it works

  1. Read

    Each module tells you which book chapters to read and the key ideas to look for.

  2. Solve

    Work in Exercises/ in VS Code, or straight in your browser with the Lean playground.

  3. Check

    lake exe check tells you which exercises are solved. It never compares your answer with the solution as text: any correct proof counts.

$ lake exe check Logic
Logic (Exercises/Logic.lean)
  ✅ ex1
  ✅ ex2
  ❌ ex3: error at line 76: Type mismatch …
  ⏳ ex4: still has `sorry`
  ⏳ ex5: still has `sorry`
  2/5 solved