Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".

Hints for challenge 5.

#check @finset.sum_range_succ might be of some use to you. Can you work out how to use it?