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

Maths challenges for the Lean curious

If you have played through the natural number game and are wondering what other mathematics can be done in Lean, you might want to try some of these challenges. The hints are essential if you are a beginner; there are no spoilers in them.

Challenge 1 (2019-12-09): the composite of injective functions is injective. There's hints and the solution.

Challenge 2 (2019-12-12): a set of reals has at most one supremum. There's hints and the solution.

Challenge 3 (2019-12-18) : two add two isn't five. There's hints and the solution.

Challenge 4 (2019-12-20) : If (g o f) is surjective then so is g. There's hints and the solution.

Challenge 5 (2019-12-23) : The sum of the first n positive odd numbers is n^2. There's hints and the solution.

Challenge 6 (2019-12-28) : An equivalence class for an equivalence relation is non-empty. There's hints and the solution.

Challenge 7 (2020-01-09) : Is there a rational number whose reciprocal is zero? There's hints and the solution.

Challenge 8 (2020-01-14) : (ghk^{-1})^{-1}=kh^{-1}g^{-1} in a group. There's hints and the solution.

Challenge 9 (2020-01-22) : V(I(V(S))) = V(S) in the theory of algebraic varieties (or in any Galois connection). There's hints and the solution.

Stuck?

If you don't want to look at the solution but have questions, you can ask questions in the #new members stream on the Lean Zulip Chat (login required, real names preferred, be nice).