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. I will try and post a few per week. The hints are essential if you are a beginner; there are no spoilers in them.
Challenge 1 (9/12/19): the composite of injective functions is injective. There's hints and the solution.
Challenge 2 (12/12/19): a set of reals has at most one supremum. There's hints and the solution.
Challenge 3 (18/12/19) : two add two isn't five. There's hints and the solution.
Challenge 4 (20/12/19) : If (g o f) is surjective then so is g. There's hints and the solution.
Challenge 5 (23/12/19) : The sum of the first n positive odd numbers is n^2. There's hints and the solution.
Challenge 6 (28/12/19) : An equivalence class for an equivalence relation is non-empty. There's hints and the solution.
Challenge 7 (9/1/20) : Is there a rational number whose reciprocal is zero? There's hints and the solution.
Challenge 8 (14/1/20) : (ghk^{-1})^{-1}=kh^{-1}g^{-1} in a group. There's hints and the solution.
Challenge 9 (22/1/20) : V(I(V(S))) = V(S) in the theory of algebraic varieties (or in any Galois connection). There's hints and the solution.
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).
Here are the Lean files for the questions and solutions.
Link to this page: tinyurl.com/LeanMathsChallenges