Proofs about your programs
Return to the functions and data of Lean foundations and prove facts about them for every input, not one example. Each lesson adds one tool and shows exactly what it leaves behind: unfold to look inside a definition, simp to simplify, omega for arithmetic, hypotheses that decide an if, cases and contradiction for your own types. Then write statements yourself, put a small verified file together, and finish with a review without step-by-step guidance.
Progress is kept in this browser until you sign in
- Look inside a definitionNewunfold replaces a name by its body, so you can reason about what it does.12 min
- Let the simplifier workNewsimp rewrites with hundreds of known facts. Read what it leaves.14 min
- Arithmetic on autopilotNewomega proves whole-number arithmetic from your hypotheses, or shows a counterexample.14 min
- Prove which branch runsUse a hypothesis to decide the condition of an if, for every input.14 min
- Prove every caseSplit a value of your own type into cases; close impossible ones with contradiction.16 min
- State your own theoremWrite inputs, a hypothesis and a claim. The proofs are supplied; the statements are yours.18 min
- Put a small file togetherA structure, a function, a test and a theorem in one file you can take home.16 min
- Review: pick the right toolNewMixed proofs about lights and fees, with no step checklist.18 min