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 135 short lessons. Write your own Lean code, check it, and learn from the result.

Start learning freeSee all courses
  • 43 lessons free
  • 135 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

14 courses in 5 stages. Each one builds on the one before it. The first 4 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 steps, proofs about your own programs, and propositional logic.

    • Lean foundationsNew lessonsValues, types, functions and your own data, checked by Lean from the first minute.11 lessons · 148 min
      FreeStart
    • Your first Lean proofsRead a goal, take a proof step, and let Lean check your reasoning.13 lessons · 200 min
      FreeStart
    • Proofs about your programsNew courseProve what your functions do for every input, one tool at a time.8 lessons · 122 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 43 free lessons need no payment. One purchase opens all 14 courses, the Pass problems and unlimited compiler checks, with no ads.

€14launch price, one payment
€19 from 1 December · 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.

Some lessons moved. Is my progress still there?

Yes. In November 2026 the proof lessons of Lean foundations moved to the new course Proofs about your programs, and every lesson you completed still counts under its new address. Old links lead to the new pages.

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.