The Natural Number Game is a Lean4 tutorial hosted on the Lean Game Server, requiring JavaScript to run. It is maintained by Marcus Zibrowius at Heinrich-Heine-Universität Düsseldorf in Germany.