Lean4
Lean 4 · Interactive course

Learn Lean by writing code and proofs.

Start with a calculation you can prove. Work up to logic, induction and verified programs through 130 short lessons. Write your own Lean code, check it, and learn from the result.

Start learning freeSee all courses
  • 38 lessons free
  • 130 exercises
  • Lean 4.30 compiler
  • Browser based no setup

Try it here. A test can reverse a few lists twice and compare. Lean can show it holds for every list, including ones nobody has written yet. Type simp in the editor and press Check.

Reverse.lean
1-- [1, 2, 3].reverse is [3, 2, 1].
2-- Reverse it again and you are back where you started.
3
4theorem reverse_twice (xs : List Nat) :
5 xs.reverse.reverse = xs := by
given
Loading editor…

The goal: for any list of numbers xs, reversing it twice gives xs back.

xs:List Nat
⊢xs.reverse.reverse = xs
Ready to checkLean 4.30
No account needed to try.

The course, in order

13 courses in 5 stages. Each one builds on the one before it. The first 3 are free; if you already know the early material, start wherever you need. See every lesson on one page →

  1. 1

    Start here

    Lean as a language, the first proof tactics, and propositional logic.

    • Lean foundationsValues, types and functions, your own data types, and the first proofs about them.14 lessons · 220 min
      FreeStart
    • Your first Lean proofsRead a goal, take a proof step, and let Lean check your reasoning.13 lessons · 200 min
      FreeStart
    • Propositional logicAnd, or, not and if-and-only-if, then excluded middle and proof by contradiction.11 lessons · 165 min
      FreeStart
  2. 2

    Proof techniques

    Quantifiers, rewriting, simp, omega and calc, and proofs written as terms.

  3. 3

    Programs and induction

    Recursive programs, induction on numbers, lists and trees, and specifications you prove.

  4. 4

    Natural Number Lab

    Arithmetic built from zero and successor, through order and divisibility.

    • The Natural Number LabAddition, multiplication, powers, order and divisibility, proved from zero and successor.18 lessons · 336 min
      PassView
  5. 5

    Advanced proofs and effects

    Proof-carrying data, length-indexed vectors, monads and their laws.

    • Advanced functional proofsLaws for map, filter and fold, evidence carried in data, and lengths checked by the type.7 lessons · 156 min
      PassView
    • Monads and effectsOption, Except, state and IO, the Monad class, and proofs of the monad laws.11 lessons · 250 min
      PassView
Academy Pass

Open every course and problem.

The 38 free lessons need no payment. One purchase opens all 13 courses, the Pass problems and unlimited compiler checks, with no ads.

€10one payment
Permanent access · No subscription
See pricingBrowse problems

Questions

Do I need to install Lean?

No. The course editor runs in the browser and sends checks to Lean 4.30. You can install Lean locally later without changing the language or tactics you learned here.

Is this Mathlib?

The exercises use Lean’s core library so that they run fast and teach the language itself. Every tactic covered (rw, simp, omega, induction, obtain, calc …) is the same one you will use with Mathlib.

When is an exercise complete?

The proof must compile without errors or sorry. Completion is then saved to your account.

What happened to the previous Lean 4 course?

Its material now belongs to the Academy sequence. Lean foundations contains the free introduction; Functional programming contains the later programming, recursion and type-class lessons.