This is the lean4 version of the classical Natural Number Game. It uses the Lean4 Game Engine and is running live at adam.math.hhu.de.
The game was initially designed for lean3 and has been adapted for lean4. See lean3 version.
You can develop the game as any lean project and use lake build to build it.
Moreover, there are multiple ways to run the game while developing it, which are described in Running Games Locally
PRs/Issues fixing typos, inconsistencies, missing hints, etc. are very welcome!
See Creating a Game at the lean4game repo for a detailed explanation.