01Free
Lean foundations
Meet Lean as a language, learn its core types, and build your first programs.
- 7 lessons
- 67 min
- 7 checked exercises
Lean 4 · Interactive course
Learn Lean by writing code and proofs.
Work through 67 lessons covering the language, tactics, induction, verified programs and proof terms. The built-in editor shows Lean’s goals and errors as you work.
- 21 lessons free
- 67 exercises
- Lean 4.30 compiler
- Browser based no setup
01
Write
Syntax highlighting, tactic completion and Lean’s Unicode abbreviations in a focused editor.
02
Inspect
Open goals, compiler errors and output stay beside the exercise that produced them.
03
Understand
Short explanations, worked examples, hints and questions connect each proof step to the idea behind it.
Course sequence
From syntax to proof terms
Follow the order or begin with the topic you need.
- 01Lean foundations3 courses · FreeCore syntax, proof goals and propositional logic.
- 02Proof techniques3 courses · PassQuantifiers, rewriting, automation and induction.
- 03Programs and data3 courses · PassFunctions, recursive programs, structures and specifications.
- 04Proof terms1 course · PassProofs as terms and the Curry–Howard correspondence.
Beginner
No experience needed. 3 full courses are free.
02Free
Your first Lean proofs
Read a goal, take a proof step, and let Lean check your reasoning.
- 6 lessons
- 53 min
- 6 checked exercises
03Free
Propositional logic, step by step
Or, not, if-and-only-if: the connectives behind every argument.
- 8 lessons
- 74 min
- 8 checked exercises
04Pass
For all, there exists
Statements about every number and about some number.
- 6 lessons
- 58 min
- 6 checked exercises
Intermediate
The tactics and techniques used in real developments.
05Pass
Rewriting, simplification, automation
The everyday tactics that do most of the work in real developments.
- 8 lessons
- 77 min
- 8 checked exercises
06Pass
Functional programming patterns
Functions as values, structured data, recursion, termination, and type classes.
- 7 lessons
- 80 min
- 7 checked exercises
07Pass
Induction on numbers and lists
Prove facts about every natural number and every list.
- 6 lessons
- 78 min
- 6 checked exercises
08Pass
Programs with proofs
Define functions and prove small, useful properties of their behavior.
- 8 lessons
- 79 min
- 8 checked exercises
09Pass
Inductive types and case analysis
Model your own data, then reason about every shape it can take.
- 5 lessons
- 57 min
- 5 checked exercises
Advanced
See the terms behind the tactics.
10Pass
Proof terms and Curry–Howard
Proofs are programs. Write them directly as terms.
- 6 lessons
- 56 min
- 6 checked exercises
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 patterns contains the later programming, recursion and type-class lessons.