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 3.

So the goal is to prove that the real number 2 + 2 isn't 5. You don't want to do this by logical first principles because the real number 2 is an infinite equivalence class of Cauchy sequences! We want to treat it as a mathematical object rather than thinking about the complicated way it has been constructed using foundations.

There is a special mathlib tactic which is designed to prove things like this. It can handle extremely large integers, rational numbers and real numbers. Instead of struggling with goals like this, you just have to know the tactic to use.

A big list of the tactics available to users is here, and it hopefully is not too hard to sopt the one you want.