Programs with proofs
Lean is a programming language. You will write functions, structures and pattern matches, then prove that they compute the right thing: specifications by rfl and decide, algebraic laws by unfolding, and case analysis on inputs.
Sign in to track your progress
- Specify a functionA theorem about a definition, proven by computation.8 min
- Reason about listsLibrary facts about append and length, applied by simp.9 min
- Compose verified stepsUnfold two applications of a function and finish the arithmetic.10 min
- State an invariantAn update never decreases a counter.9 min
- Safe division with OptionSpecify a partial function that returns none instead of failing.11 min
- Case analysis on inputsProve a fact about a pattern-matching function with cases.12 min
- Check every Booleancases b <;> rfl proves a law for both truth values.9 min
- Structures and round tripsSwapping a point twice returns the original point.11 min