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.
If you want to contribute to the Natural Number Game, it is probably best if you ask us for access and push on a non-main branch in this repo. That way a github-action will build the game automatically.
See the documentation for an explanation of the game commands.
In order to create a new game, click "use this template" above to create your own game. That way there is a github action that can build a docker image from your main branch which can be used to add the game to the server at adam.math.hhu.de.
Note that the setup is currently still in development and will likely see changes and improvements in the next few months. In particular, you need to change the game's name in several places inside the code when creating a new one.