You might enjoy http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game...

It's a game implemented in lean, where you work your way through the basic facts about natural numbers.