A Lean 4 Proof Gym
Progressive exercises in formal proof. Start from True, build to real analysis. You don't understand a theorem until you've proved it yourself.
Each exercise explains the concept — what the theorem means, why it matters, and the intuition behind it.
Translate your understanding into a formal Lean 4 proof. Start with the skeleton, fill in the tactics.
Paste into Lean 4 Web or your local VS Code. If Lean accepts it, you've proved it.
Each track is a sequence of lessons and exercises, ordered by difficulty. Learn the maths, then prove it.
Propositional logic, implications, if-and-only-if, negation, classical reasoning.
6 exercisesPeano axioms, induction, addition, multiplication, ordering.
5 exercisesMembership, subsets, union, intersection, complements, power sets.
coming soonInjectivity, surjectivity, composition, inverse functions.
coming soonGroups, rings, homomorphisms, quotients.
coming soonLimits, continuity, sequences, series, the reals.
coming soonNone beyond basic arithmetic. We teach the maths as we go. That's the point.
Helpful but not required. If you've used any programming language, Lean's syntax will feel familiar.
A browser. Use Lean 4 Web to check your proofs. Or install Lean 4 + VS Code locally for a better experience.