The Natural Number Game

https://adam.math.hhu.de/#/g/leanprover-community/nng4

A gamified tutorial for the Lean theorem prover, very close to an Interactive explainer for Lean