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

#print equivalence will tell you Lean's definition of an equivalence relation.

If you write write #check ne_empty and then hold down ctrl and hit space, you will see the names of all the theorems which have ne_empty in their name. You might want to do this because the goal is to prove that a set is Not Equal to the EMPTY set. Alternatively you can search the docs! That's a link to the basic interface for sets. An example of something useful you'll find there is the theorem ne_empty_iff_exists_mem.