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