Lean 4 Game

This is the source code for the Lean Game Server hosted at adam.math.hhu.de.

Creating a Game

Please follow the tutorial Creating a Game. In particular, the following steps may be of interest:

Documentation

The documentation is very much work in progress but the links below should be up-to-date:

Game creation API

Creating a Game: the main document to consult.
More about Hints: describes the Hint and Branch tactics.

Frontend API

How to Run Games Locally: play a game on your computer
How to Update an existing Game: update to a new lean version
How to Publish a Game: load your game to adam.math.hhu.de for others to play

Backend

Server: describes the server part (i.e. the content of server/ and relay/).

Hosting

How to host a lean4game instance yourself: how to set up your own Lean Game Server

Contributing

Contributions to lean4game are always welcome!

Translation

We welcome translations of the game interface and of the various games hosted on the Lean Game Server into different languages!

For translating the interface, please refer to these instructions.
For translating individual games, please contact the maintainers (see table below) and consult any game specific translation guidelines. Our generic guidlines may give a rough indication of the steps involved.
We also have some guidelines for game maintainers regarding translations.

Security

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.

Contact

In case of a server outage at adam.math.hhu.de please open an issue and/or contact us by <a href="mailto:adam@math.hhu.de?subject=Server Outage">email</a>. Bug reports and feature requests regarding the game interface should be filed on the issues page of this repository. For specific games on the Lean Game Server, please refer to the github repositories linked to below or contact the maintainers.

Game/repository	Maintainer
Knights and Knaves	Jad Abou Hawili
Linear Algebra Game	ZRTMRH
Logic Game	Trequetrum
Natural Number Game (NNG)	Kevin Buzzard
Real Analysis Game	Alex Kontorovich
Reintroduction to Proofs	Emily Riehl
Robo / Scribble	Marcus Zibrowius
Set Theory Game	Dan Velleman

Credits

The project has primarily been developed by Alexander Bentkamp and Jon Eugster.

It is based on ideas from the Lean Game Maker and the Natural Number Game
(NNG)
by Kevin Buzzard and Mohammad Pedramfar, and on Patrick Massot's prototype: NNG4.