Yes, this exists. it is called the "Natural Number Game" and interactively teaches you to use the Lean theorem prover to prove simple theorems about addition, multiplication, and so on. It runs in the browser.

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_gam...