Skip to content

leanprover-community/lean4game

Repository files navigation

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

Frontend API

Backend

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

Hosting

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!

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 technical problems with/outages of the server at adam.math.hhu.de please contact Matvey Lorkish.

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 Slaves 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.