This is the source code for a Lean 4 game platform hosted at adam.math.hhu.de.
Please follow the tutorial Creating a Game. In particular, the following steps might be of interest:
- Step 5: How to Run Games Locally
- Step 7: How to Update an existing Game
We encourage anybody to have games hosted on our Lean Game Server for anybody to play. For that you simply need to contact us with the link to your game repo. We are also happy to add work-in-progress games and games in any language.
For example, you can contact Jon on Zulip. Or via Email.
The documentation for the game engine itself is still missing, but there is Creating a Game explaining the API to create a game.
Some documentation:
Contributions to lean4game are always welcome!
Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server with bubblewrap.
The project is based on ideas from the Lean Game Maker and the Natural Number Game (NNG) of Kevin Buzzard and Mohammad Pedramfar. The project is based on Patrick Massot's prototype: NNG4.