Lean foundations
Learn Lean as a programming language first. Check a first claim, read every kind of reply Lean gives, evaluate and inspect expressions, choose the right type, write functions with conditions, and model data with structures, inductive types, lists and optional values. Every check runs on concrete values, so nothing depends on a proof technique you have not met yet. Each 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 proof experience is assumed.
Progress is kept in this browser until you sign in
- Your first checked statementRead a claim, write rfl, and let Lean check it.8 min
- Evaluate and inspectRun a calculation with #eval and ask for its type with #check.10 min
- Read Lean’s replyRewrittenThe four replies you will see most, word for word, and what to do about each.12 min
- Ask Lean about typesRead the type of a function, and tell data apart from claims.12 min
- Numbers, text and true or falseNat, Int, Bool and String, and the subtraction that stops at zero.14 min
- Write your own functionParameters, a result type Lean holds you to, and checks that call your code.14 min
- Choose with ifNewFunctions that decide: if, then, else, comparisons and several cases.14 min
- Group values in a structureNamed fields, building records, and updating one field.14 min
- Define your own choicesAn inductive type lists every possible value; pattern matching handles each one.15 min
- Lists and missing valuesRewrittenLists, their two shapes, and Option for a value that may be absent.15 min
- Review: build it without helpRewrittenDefine a type, a record and functions on them, and predict their output, with no step checklist.20 min