Real-time collaboration for Jupyter Notebooks, Linux Terminals, LaTeX, VS Code, R IDE, and more,
all in one place. Commercial Alternative to JupyterHub.

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

If you've done inequality world in the natural number game then you'll know about the use tactic and you shouldn't have too much trouble with this level. If you're not sure how surjective is defined in Lean then unfold surjective will tell you.