Buy the course once.
The first 3 courses are free. A single payment opens the remaining 7 courses permanently. Compiler checks can be added separately whenever you need them.
Start with Lean
Programming foundations, first proofs and propositional logic.
- Courses
- 3
- Lessons
- 21
- Compiler checks
- 40 / month
- Advertising
- Shown
The complete course
Permanent access. No renewal and no subscription to cancel.
- Courses
- All 10
- Lessons
- All 67
- Included checks
- 500
- Advertising
- None
500 checks for €5
Credits do not expire. Your monthly free checks are always used first.
Course access
21 lessons are free. The pass adds 46.
| Course | Level | Lessons | Access |
|---|---|---|---|
| Lean foundations | Beginner | 7 | Free |
| Your first Lean proofs | Beginner | 6 | Free |
| Propositional logic, step by step | Beginner | 8 | Free |
| For all, there exists | Beginner | 6 | Academy Pass |
| Rewriting, simplification, automation | Intermediate | 8 | Academy Pass |
| Functional programming patterns | Intermediate | 7 | Academy Pass |
| Induction on numbers and lists | Intermediate | 6 | Academy Pass |
| Programs with proofs | Intermediate | 8 | Academy Pass |
| Inductive types and case analysis | Intermediate | 5 | Academy Pass |
| Proof terms and Curry–Howard | Advanced | 6 | Academy Pass |
Prices include applicable tax. Stripe shows the final total before payment. Purchases are covered by the withdrawal and refund policy.
Questions
Is this a subscription?
No. The Academy Pass is a one-time purchase. Course access does not expire.
When are purchased checks used?
Each account receives 40 free checks per calendar month. After those are used, the compiler draws from purchased credits. A failed proof counts as a check; a server failure does not.
What runs in the playground?
Lean 4.30 with its core library. Mathlib, package installation and network access are not available in the hosted compiler.
What remains free?
The language guide, tactic reference, forum and the Academy’s first 3 courses remain free.