If you have played addition world, multiplication world and power world, you have basically
learnt three tactics: rw, induction and refl. These only get you so far -- you can
develop "equational theories" but you cannot prove any implications.
However if you've done things like proposition world you will also know about tactics
such as apply, intro and exact, and with these tactics you can do a whole lot more
mathematics. For example you can probably do many of the Lean maths challenges on cocalc or using the Lean web editor. These are undergraduate level mathemamatics challenges involving equivalence relations, group theory and so on.
At the time of writing there are still around 30 perfectoid space levels. You'll need to know a whole bunch of Lean and also a whole bunch of commutative algebra to do these. Once we've done all of them, we will get a formally verified example of a non-empty perfectoid space. This is a research project, but it's certainly accessible.
I (Kevin Buzzard) teach an undergraduate maths course to 1st years at Imperial, and I have been formalising the example sheets. You can try these if you know undergraduate level mathematics.
More of my hopes and dreams are listed here. This list gets added to far more often than things are removed from it. That is the nature of the game at this point in time. Things will change.
Finally, there are often problems kicking around on the Zulip Lean chat. Login required, real names preferred, be nice.
Kevin Buzzard, in lockdown, 30th March 2020.