Your first Lean proofs
Start from zero. You will learn how a Lean theorem is written, how to read the goal and hypotheses, and how five fundamental tactics let you finish real proofs on your first day.
Sign in to track your progress
- Equality by computationWhat a theorem looks like, and why rfl closes 3 + 4 = 7.8 min
- Use what you already knowHypotheses are proofs you already hold. exact hands one to Lean.7 min
- Prove an implicationAssume the premise with intro, then prove the conclusion.9 min
- Build a two-part proofconstructor splits P ∧ Q, bullets keep the branches tidy.9 min
- Apply an implicationAn implication is a function on proofs. apply works backwards from the goal.10 min
- Take a hypothesis apartobtain ⟨hp, hq⟩ := h unpacks a conjunction so you can use both halves.10 min