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!
We happily accept translations of the game into different lanugages! You can use .i18n/en/Game.pot
and translate it into .i18n/{lang}/Game.po
where {lang}
is the ISO language code like fr
or en_UK
, using for example POEdit.
We would like the following requirements for a translation PR:
See Creating a Game at the lean4game repo for a detailed explanation.