A gamification of some theorems and problem sheet questions in MATH40002 Analysis 1.
A sequel to the Natural Number Game, the Real Number Game is an attempt to teach Imperial's 1st year undergraduates (and anyone else who wants to join in) the rudiments of real analysis via the Lean Theorem Prover.
Planned sections so far:
- Sup and Inf -- see
world_plans/supinf.lean - Sequences and limits
- Series and sums