Start free. Pay once to finish.
Lean foundations, Your first Lean proofs and Propositional logic are free. The Academy Pass costs €10, paid once, and opens the other 10 courses: about 24 hours of exercises.
Start with Lean
Lean foundations, first proofs and propositional logic.
- 3 courses, 38 lessons
- 10 checks to try it without an account
- 40 checks a month with a free account
- Progress saved to your account
- Easy problems and the daily problem on Problems
The complete Academy
No subscription and nothing to cancel.
- All 13 courses, all 130 lessons
- Unlimited compiler checks
- Induction, the Natural Number Lab, verified programs, monads and more
- Every problem on Problems
- No advertising anywhere on lean4.dev
- Permanent access
You can withdraw within 14 days from your account. How refunds work
What the Pass opens
38 lessons are free. The Pass adds 92.
| Course | Level | Lessons | Access |
|---|---|---|---|
| Lean foundations | Beginner | 14 | Free |
| Your first Lean proofs | Beginner | 13 | Free |
| Propositional logic | Beginner | 11 | Free |
| Quantifiers | Beginner | 7 | Academy Pass |
| Rewriting and automation | Intermediate | 8 | Academy Pass |
| Proof terms and Curry–Howard | Intermediate | 7 | Academy Pass |
| Functional programming | Intermediate | 12 | Academy Pass |
| Induction on numbers and lists | Intermediate | 6 | Academy Pass |
| Programs with proofs | Intermediate | 9 | Academy Pass |
| Inductive types and case analysis | Intermediate | 7 | Academy Pass |
| The Natural Number Lab | Intermediate | 18 | Academy Pass |
| Advanced functional proofs | Advanced | 7 | Academy Pass |
| Monads and effects | Advanced | 11 | 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 and nothing renews.
What does “unlimited checks” mean?
Check your code as often as you need, including every failed attempt. A fair-use limit of 300 checks a day stops runaway scripts; it resets at midnight UTC and a learner working through lessons does not reach it.
What counts as a check on the free plan?
Each time you press Check, Run or Submit, whether the proof succeeds or not. A server failure does not count. Free checks reset at the start of each month, and the editor on the Academy homepage never uses them.
Can I get my money back?
Yes. Within 14 days of buying you can withdraw online from your account and the payment is refunded to the original method. See the withdrawal page.
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, the Academy’s first 3 courses, and the Easy and daily problems remain free.