Start free. Go further with Pro.
A complete introductory course is free. Pro adds practical proof patterns and verified programming, with more room to experiment.
Free
- 4 introductory lessons and exercises
- Hints, solutions, and saved progress
- 30 compiler checks each month
- All existing reference guides
Pro
- All 3 published courses, 12 lessons total
- All exercises, hints, and explained examples
- 1,000 compiler checks each month
- Saved course progress across devices
- Cancel renewal from your account
Pro renews monthly until canceled. The advertised price includes applicable taxes. Your checkout shows the total before you pay. Canceling renewal keeps access until the end of the paid period.
How do compiler allowances work?
A check runs your code once, for up to 15 seconds. Failed proofs also use a check. Allowances reset on the first day of each month at 00:00 UTC and do not roll over. One check can run per account at a time. The platform has a shared monthly capacity limit; checking may pause if it is reached. Reading lessons remains available.
What can I run?
The playground uses Lean 4.30.0 and its bundled core libraries. It supports small programs and proofs. Installing packages, network access, and full Mathlib projects are not included in this initial release.
What stays free?
The existing language guide, reference course, and tactic reference stay free. The introductory interactive course is also free; an account with a verified email is required to use the hosted compiler.