Lean Game Server
Welcome to the Lean Game Server where you can find interactive learning
games about Lean.
Formaloversum
Erkunde das Leansche Universum mit deinem Robo,
welcher dir bei der Verständigung mit den Formalosophen zur Seite steht.
Dieses Spiel führt die Grundlagen zur Beweisführung in Lean ein und schneidet danach
verschiedene Bereiche des Bachelorstudiums an.
(Das Spiel befindet sich noch in der Entstehungsphase.)
Das Spiel wurde im Rahmen des Projekts ADAM
an der HHU in Düsseldorf
entwickelt.
| Prerequisites |
- |
| Worlds |
? |
| Levels |
? |
| Language |
🇩🇪 |
Natural Number Game
The classical introduction game for Lean.
In this game you recreate the natural numbers
\(\mathbb{N}\) from the Peano axioms, learning the basics
about theorem proving in Lean.
This is a good first introduction to Lean!
| Prerequisites |
- |
| Worlds |
9 |
| Levels |
72 |
| Language |
🇬🇧 |
Adding new games
If you consider writing your own game, you should use the
NNG Github Repo
as a template.
There will be an option to load and run games through the server
directly by specifying a URL, but this is still in development.
To add games to this page, you should get in contact as
games will need to be added manually.
Impressum
When running a game, our server collects metadata
(such as IP address, browser, operating system)
and the data that the user enters into the editor.
The data is used to compute the Lean output and display it to the user.
The information will be stored as long as the user stays on our
website and will be deleted immediately afterwards.
We keep logs to improve our software, but the contained
data is anonymized.
We do not use cookies, but the game progress is stored in the
browser as site data. The game progress is not saved on the server;
if you delete your browser storage, it will be completely gone.
Our server is located in Germany.
Contact information
Jon Eugster
Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf
Universitätsstr. 1
40225 Düsseldorf
Germany
Contact Details