Read. Try. Understand.
Learn Lean by writing proofs that work.
Short explanations and focused exercises, with a Lean compiler beside you. Start with your first proof, then build the patterns behind reliable programs.
Your first Lean proofs
Read a goal, take a proof step, and let Lean check your reasoning.
Explore coursePractical proof patterns
Rewrite equations, simplify goals, split cases, and automate arithmetic.
Explore coursePrograms with proofs
Define functions and prove small, useful properties of their behavior.
Explore courseA clear path from reading to doing
Each lesson introduces one idea, shows a worked example, and gives you a new goal to prove. Check your attempt, read Lean’s feedback, and use a hint when you need one. Sign in to save completed exercises across devices.
The existing reference course and tactic guides remain free.