The Natural Numbers Game is amazing, highly recommended.

> In this game you recreate the natural numbers N from the Peano axioms, learning the basics about theorem proving in Lean.

https://adam.math.hhu.de/