This library renders structured Lean files into an interactive game with a javascript Lean server running on the browser. See the Natural number game for an implementation of this game.
The games built with this library work best in Chrome and Firefox.
See the installation guide.
See the usage guide.
This fork aims at adding new features to the great original project of mpedramfar:
- Hinted proofs: parts of the proof are shown to the player, who only needs to complete the remaining sorry(s).
- View Source: A new button that opens the source of the current level in a Lean Web Editor, to make it easy to modify and add new levels to a game.