Lean4
Lean4 Academy

All lessons

130 lessons in 13 courses, about 34 hours in total. 38 lessons are free; the Academy Pass opens the rest. Each lesson ends with an exercise the Lean compiler checks.

Start here

Lean foundations

14 lessons · 220 min

Free
  1. Your first checked statementRead a theorem, write rfl, and check a proof of a calculation.11 min
  2. Evaluate and inspectRun a calculation with #eval and inspect its type with #check.12 min
  3. Ask Lean about typesUse #check to read a type, and tell data apart from statements.14 min
  4. Values and core typesNat, Int, Bool, and the truncated subtraction that catches everyone once.15 min
  5. Write your own functionParameters, a result type Lean holds you to, and checks that call your code.16 min
  6. Prove which branch runsUnfold a function and use a hypothesis to simplify its condition.15 min
  7. Lists and optional valuesProve the first-element law for every nonempty list.15 min
  8. Model data with a structureDefine named fields, construct records and update one field safely.17 min
  9. Define data by constructorsCreate a three-state type and write an exhaustive transition function.17 min
  10. Prove every constructor caseSplit an arbitrary value into cases and prove a property in every branch.17 min
  11. Read and repair an errorPreserve the valid part of a multi-step proof and repair its first error.14 min
  12. State your own theoremWrite binders, a hypothesis and a claim. The proofs are supplied; the statements are yours.19 min
  13. Put a small file togetherCombine a structure, record update, evaluation and multi-step theorem.18 min
  14. Review: build it without helpDefine a type and functions, prove properties by cases and predict output, with no step checklist.20 min

Your first Lean proofs

13 lessons · 200 min

Free
  1. Equality with an unknown inputProve n + 0 = n and learn when computation can work with a variable.13 min
  2. Use what you already knowHypotheses are proofs you already hold. exact hands one to Lean.12 min
  3. Prove an implicationAssume the premise with intro, then prove the conclusion.14 min
  4. Build a two-part proofconstructor splits P ∧ Q, bullets keep the branches tidy.14 min
  5. Apply an implicationAn implication is a function on proofs. apply works backwards from the goal.15 min
  6. Name an intermediate stephave records a fact you have derived, so later steps can use it by name.15 min
  7. Take a hypothesis apartobtain ⟨hp, hq⟩ := h unpacks a conjunction so you can use both halves.15 min
  8. Plan a proof, then fill it inWrite the structure first with sorry in the holes, and let Lean show what each hole needs.17 min
  9. Replace equals by equalsrw [h] substitutes using an equation, even inside functions no tactic can compute.15 min
  10. Rewrite through a chainRecord each step of an equality argument in a readable calc proof.17 min
  11. Prove both Boolean casesSplit an arbitrary Boolean and verify both exhaustive branches.15 min
  12. Practice: transform both sidesUnpack, split and apply two implications in a branching proof.20 min
  13. Review: choose the next moveMixed exercises from the whole course, with no step checklist.18 min

Propositional logic

11 lessons · 165 min

Free
  1. Prove an or-statementTo prove P ∨ Q, pick the side you can prove.12 min
  2. Reason from alternativescases h with | inl hp | inr hq handles both possibilities.16 min
  3. What ¬P really meansA negation is a function into False. Apply it like one.14 min
  4. From a contradiction, anythingexfalso and absurd let a contradiction prove any goal.14 min
  5. Prove an equivalenceP ↔ Q is two implications. constructor gives you both.13 min
  6. Use an equivalenceh.mp and h.mpr turn an iff into the direction you need.13 min
  7. Prove a contrapositiveFrom P → Q and ¬Q, build ¬P by introducing an assumed P.15 min
  8. A De Morgan lawShow ¬(P ∨ Q) gives ¬P ∧ ¬Q, combining everything so far.17 min
  9. Split on whether P holdsby_cases and the classical De Morgan law ¬(P ∧ Q) → ¬P ∨ ¬Q.17 min
  10. Proof by contradictionAssume the negation of the goal, derive False, and see why that step is classical.16 min
  11. Review: every connectiveMixed exercises on or, not, iff and classical reasoning, with no step checklist.18 min

Proof techniques

Quantifiers

7 lessons · 107 min

Pass
  1. Prove a statement about every numberintro n picks an arbitrary n. Whatever you prove holds for all of them.15 min
  2. Use a universal hypothesisA ∀-hypothesis is a function: apply it to the value you need.13 min
  3. Provide a witnessTo prove ∃ n, …, name the n and prove the property for it.14 min
  4. Use an existential hypothesisobtain ⟨n, hn⟩ := h gives you the witness and its property.16 min
  5. Specialize a hypothesisNarrow a general fact to the one instance your goal needs.14 min
  6. Combine both quantifiersBuild an existence proof whose witness comes from a hypothesis.17 min
  7. Review: four quantifier movesIntroduce, apply, witness and open quantifiers in mixed exercises, with no step checklist.18 min

Rewriting and automation

8 lessons · 77 min

Pass
  1. Rewrite with an equalityrw [h] replaces the left side of h by its right side everywhere.9 min
  2. Rewrite in the other directionrw [← h] uses an equation right-to-left. Chain rewrites in one call.10 min
  3. Rewrite inside a hypothesisrw [h] at h2 changes a hypothesis instead of the goal.9 min
  4. Simplify a goalsimp normalizes with hundreds of known lemmas.8 min
  5. Point simp and rw at the right lemmasLibrary lemmas about lists and arithmetic, used by name.12 min
  6. Decide a finite factdecide evaluates a decidable proposition and produces a proof.8 min
  7. Linear arithmetic with omegaInequalities and natural-number subtraction, solved automatically.9 min
  8. Chain equalities with calcA readable proof that shows each rewriting step and its justification.12 min
Pass
  1. An implication is a functionfun hp => hp proves P → P.9 min
  2. A conjunction is a pair⟨hp, hq⟩ proves P ∧ Q.8 min
  3. Projectionsh.1 and h.2 read the halves of a conjunction.8 min
  4. Compose implicationsChaining P → Q and Q → R is function composition.10 min
  5. Eliminate a disjunctionh.elim takes one handler per case.11 min
  6. Existentials as dependent pairs⟨witness, proof⟩ proves ∃ n, p n.10 min
  7. Assemble a whole proof termName every component, then hand Lean one finished term.14 min

Programs and induction

Functional programming

12 lessons · 148 min

Pass
  1. Functions as valuesPass behaviour as an argument, then prove a law about every input.10 min
  2. Functions you build as you goCapture local context in a lambda, and return a function as a result.11 min
  3. Structures and record updatesNamed fields, precise copies, and why eta closes a round trip.11 min
  4. Define your own structureFields, the constructor Lean generates for you, and record updates.12 min
  5. Exhaustive pattern matchingWildcards, exhaustiveness, and covering every constructor in a proof.12 min
  6. Recursion on natural numbersBase and successor cases, and the equations they hand you for free.12 min
  7. Recursion on listsPeel constructors off a list while staying polymorphic in the elements.12 min
  8. Write and verify your own mapBuild a polymorphic higher-order list function, then prove that it preserves length.18 min
  9. Walk two lists at onceMatch two lists together and combine them element by element.13 min
  10. Why recursion must terminateWhat Lean rejects, why it must, and what totality buys your proofs.10 min
  11. Recursion that is not structuralRecursive calls on computed values, and the measure that proves they stop.14 min
  12. Classes and instancesDescribe shared behaviour and let Lean pick the implementation.13 min
Pass
  1. Your first inductionProve double n = n + n for a recursive double.14 min
  2. Why 0 + n = n needs inductionn + 0 is rfl, 0 + n is not. See what computation does and does not give you.13 min
  3. Induction over listsA hand-written length distributes over append.15 min
  4. map preserves lengthBase cases that compute, step cases that rewrite.12 min
  5. A growth bound by inductionThe sum 0 + 1 + … + n is at least n.12 min
  6. Exponential growthProve n < 2ⁿ with an induction hypothesis and omega.12 min

Programs with proofs

9 lessons · 127 min

Pass
  1. Specify a functionThree properties that pin down a maximum, and split for the proof.12 min
  2. Safe division with OptionSpecify a partial function that returns none instead of failing.11 min
  3. Case analysis on inputsProve a fact about a pattern-matching function with cases.12 min
  4. Structures and round tripsSwapping a point twice returns the original point.11 min
  5. Verify your own reverseReversing a concatenation reverses the order of the pieces, by induction.15 min
  6. Build on a proved lemmaReversing twice gives back the list, with the previous law doing the hard step.13 min
  7. A Boolean search over a listSearching two joined lists is searching each part and combining with ||.13 min
  8. An invariant over every runA capped counter stays within its cap after any sequence of operations.16 min
  9. Project: verified iterationWrite a polymorphic iterator, prove its composition law, and verify a numeric specialization.24 min
Pass
  1. An enumeration and a general cycle lawTraffic lights: define a transition and prove its cycle for every constructor.12 min
  2. Define your own typeDeclare constructors, match on all of them, and meet the missing-case error.11 min
  3. Prove two-sided inverse operationsShow next and previous cancel in both orders across every constructor.13 min
  4. Constructors that carry dataShapes with sizes, and a scaling law proven per constructor.12 min
  5. Binary treesEvery tree has positive size.11 min
  6. Induction over treesTwo induction hypotheses, one for each subtree.14 min
  7. Derive the fold for your own typeOne function parameter per constructor, read straight off the declaration.15 min

Natural Number Lab

The Natural Number Lab

18 lessons · 336 min

Pass
  1. Addition worldAddition from recursionStart from zero and successor, then prove the first identity by induction.15 min
  2. Move a successor across additionProve the equation the recursive definition does not compute for you.16 min
  3. Addition commutesCombine the first two lemmas in a structured induction.18 min
  4. Addition associatesControl three nested unfolds and expose the induction hypothesis.18 min
  5. Cancel a common tailRewrite inside a hypothesis and recover equality of the starting values.20 min
  6. Multiplication worldZero times everythingRebuild the left-zero law directly from multiplication recursion.14 min
  7. Move a successor through multiplicationExpose recursive products, then finish the visible arithmetic.18 min
  8. Multiplication distributesProve distributivity one successor at a time without a broad simplifier.20 min
  9. Multiplication commutesPair left and right recursion laws in the induction step.18 min
  10. Multiplication associatesUse distributivity as a local step inside a larger induction.22 min
  11. Power worldAdding exponentsProve that exponent addition becomes multiplication of powers.20 min
  12. Powers of a productInduct, then commute the middle factors with a controlled normalization.22 min
  13. Order worldOrder as a gapDefine an order relation with an existential witness and prove reflexivity.14 min
  14. Compose two gapsBuild a transitivity witness and document the route with calc.20 min
  15. Two directions force equalityExpose hidden gaps and derive antisymmetry from their equations.18 min
  16. Divisibility worldCompose divisibility witnessesMultiply two quotient witnesses and associate the resulting product.20 min
  17. A divisor of a sumAdd quotient witnesses and factor the common divisor.18 min
  18. Finale: chain, add and factorSynthesize three hypotheses in a long, readable divisibility proof.25 min

Advanced proofs and effects

Advanced functional proofs

7 lessons · 156 min

Pass
  1. Higher-order listsBuild map and prove its append lawImplement a polymorphic map, then prove the compositional law callers need.20 min
  2. Fuse two mapsRemove an intermediate traversal with a general function-composition proof.16 min
  3. Fuse filtering and mappingWrite a branching list combinator and prove its append law in both predicate cases.22 min
  4. Folds and invariantsA fold with a generalized accumulatorBuild a left fold and strengthen the induction hypothesis enough to prove chunking.22 min
  5. Carry a proof for every elementDefine an indexed All predicate and map evidence through a transformation.24 min
  6. Dependent dataMake lengths part of the typeImplement vector map so preserving length is enforced before any theorem runs.24 min
  7. Verified projectFinale: verify a polymorphic tree mapProve map fusion and size preservation with two induction hypotheses per node.28 min

Monads and effects

11 lessons · 250 min

Pass
  1. Failure and sequencingOption as a monadReplace nested matches with bind and short-circuit a two-step safe division.18 min
  2. Do notation, desugaredWrite the exact >>= chain behind two left-arrow bindings.18 min
  3. Errors that carry a reasonRefactor safeDiv from Option to Except while keeping the pipeline.20 min
  4. Abstraction ladderFunctor and ApplicativeMap one contextual value and combine two independent ones.20 min
  5. Execution and performanceIO and the proof boundaryRead a file, print a result, and understand why IO stays opaque.18 min
  6. Array, List and access patternsUse array literals, map and safe indexing, then prove size preservation.20 min
  7. Mutable syntax is a foldWrite let mut and for, then prove the loop equals its fold specification.22 min
  8. Lawful effectsWrite a Monad and prove its lawsImplement a Trace monad and prove left identity, right identity and associativity.32 min
  9. StateM and a verified counterThread state through two actions and prove the state-monad laws.26 min
  10. Combine state and errors with StateTBuild a failing balance computation and reason about transformer order.26 min
  11. Dependent programsMake invalid workflows impossibleIndex commands by protocol state and prove typed composition laws.30 min