Lean foundations
The practical start of the former Lean 4 course, rebuilt as interactive Academy lessons. Explore values and types, define functions, work with lists and options, read compiler feedback, and learn how the browser workflow transfers to Lean, Lake, and VS Code.
Sign in to track your progress
- What Lean isA programming language, proof assistant, and small trusted kernel.8 min
- Evaluate and inspectUse #eval and #check, then turn an observation into a theorem.8 min
- Values and core typesNatural numbers, Booleans, strings, inference, and type errors.10 min
- Define a functionParameters, return types, application, and checked examples.10 min
- Lists and optional valuesRepresent sequences and missing results without null.12 min
- Read goals and cover casesUse compiler feedback and exhaustive case analysis on Bool.11 min
- From browser to a Lean projectTransfer the same workflow to elan, Lake, and VS Code.8 min