Natural Number Game in Verso🔗

This document is a prototype: the texts and levels come from NNG4, and the site itself is generated by Verso. Proofs are checked by the Lean server of the lean4game engine, which the editor of each level connects to via a WebSocket.

To play, click into the editor of a level and enter tactics, one per line, or click the buttons above the editor. On the right you see the goals after the line containing the cursor, with the parts changed by that line highlighted, as well as hints and error messages. Abbreviations such as \l followed by a space become ←. Your progress is stored in the browser and shown on the map: green is solved, blue is playable, grey is still locked.