Lean foundations
Start with computation, then move to general statements. Inspect values and types, define functions, model data with structures and inductive types, prove properties by simplification and case analysis, and finish with a small file that combines code, evaluation, hypotheses and rewriting. Every lesson has further exercises that ask more with less help, and the course ends with a review without step-by-step guidance. No programming or formal proof experience is assumed.
Progress is kept in this browser until you sign in
- Your first checked statementRead a theorem, write rfl, and check a proof of a calculation.11 min
- Evaluate and inspectRun a calculation with #eval and inspect its type with #check.12 min
- Ask Lean about typesUse #check to read a type, and tell data apart from statements.14 min
- Values and core typesNat, Int, Bool, and the truncated subtraction that catches everyone once.15 min
- Write your own functionParameters, a result type Lean holds you to, and checks that call your code.16 min
- Prove which branch runsUnfold a function and use a hypothesis to simplify its condition.15 min
- Lists and optional valuesProve the first-element law for every nonempty list.15 min
- Model data with a structureDefine named fields, construct records and update one field safely.17 min
- Define data by constructorsCreate a three-state type and write an exhaustive transition function.17 min
- Prove every constructor caseSplit an arbitrary value into cases and prove a property in every branch.17 min
- Read and repair an errorPreserve the valid part of a multi-step proof and repair its first error.14 min
- State your own theoremWrite binders, a hypothesis and a claim. The proofs are supplied; the statements are yours.19 min
- Put a small file togetherCombine a structure, record update, evaluation and multi-step theorem.18 min
- Review: build it without helpDefine a type and functions, prove properties by cases and predict output, with no step checklist.20 min