Your first Lean proofs
Read goals and hypotheses, then build increasingly substantial proofs. Learn the core structural tactics, unpack conjunctions, plan a proof with holes, rewrite with equations and through equality chains, reason by exhaustive cases and finish with a review that composes everything without step-by-step guidance.
Progress is kept in this browser until you sign in
- Equality with an unknown inputProve n + 0 = n and learn when computation can work with a variable.13 min
- Use what you already knowHypotheses are proofs you already hold. exact hands one to Lean.12 min
- Prove an implicationAssume the premise with intro, then prove the conclusion.14 min
- Build a two-part proofconstructor splits P ∧ Q, bullets keep the branches tidy.14 min
- Apply an implicationAn implication is a function on proofs. apply works backwards from the goal.15 min
- Name an intermediate stephave records a fact you have derived, so later steps can use it by name.15 min
- Take a hypothesis apartobtain ⟨hp, hq⟩ := h unpacks a conjunction so you can use both halves.15 min
- Plan a proof, then fill it inWrite the structure first with sorry in the holes, and let Lean show what each hole needs.17 min
- Replace equals by equalsrw [h] substitutes using an equation, even inside functions no tactic can compute.15 min
- Rewrite through a chainRecord each step of an equality argument in a readable calc proof.17 min
- Prove both Boolean casesSplit an arbitrary Boolean and verify both exhaustive branches.15 min
- Practice: transform both sidesUnpack, split and apply two implications in a branching proof.20 min
- Review: choose the next moveMixed exercises from the whole course, with no step checklist.18 min