The set theory game on the same site it also fun https://adam.math.hhu.de/ https://adam.math.hhu.de/ Another one is mathematics in lean https://leanprover-co

The set theory game on the same site it also fun https://adam.math.hhu.de/ https://adam.math.hhu.de/ Another one is mathematics in lean https://leanprover-community.github.io/mathematics_in_lean/ https://leanprover-community.github.io/mathematics_in_lean/ It's a text book with many examples for you to try. There are sample solutions which if you get stuck (which I often do) you can take a peek for some help. I actually just grep the solution file -A1 , -A2 etc to peek at the solutions one line at a time Example problems and solutions https://github.com/leanprover-community/mathematics_in_lean https://github.com/leanprover-community/mathematics_in_lean