lean4game: a self-hostable server for Lean 4 games

What lean4game actually hosts

lean4game is the source code behind a single public service, the Lean Game Server at adam.math.hhu.de, whose purpose is stated plainly in the repository description: to host Lean games. A Lean game here is an exercise for the Lean 4 proof assistant, where the player fills in or repairs a proof and the system responds by checking it.

The audience is narrow and specific. The people who benefit are the ones already teaching or practising Lean: course authors who want exercises their students can attempt without installing a toolchain, and maintainers of the individual games listed in the contact table, which includes the Natural Number Game, a Real Analysis Game, a Linear Algebra Game and a Set Theory Game, each with its own repository and named maintainer.

Two features separate this from a plain checker. The documentation includes a dedicated file on hints that describes the `Hint` and `Branch` tactics, so a game can guide a stuck player step by step rather than only reporting failure. And a published game is a live web app with a translated interface, not a file to download, which is why the project keeps translation instructions for the interface and separate guidelines for translators of individual games.

What it is not is a general purpose online Lean editor. The whole design is oriented around the game loop: a level list, a proof to complete, feedback, hints.

Three workspaces and a Lean binary behind them

The repository root shows the shape of the system. There is a `client` directory, a `relay` directory and a `server` directory, and the npm manifest declares `client` and `relay` as workspaces. The client is the browser side, and the repository topics list `react` alongside `lean4`, which matches a React frontend.

The relay sits between the browser and the Lean instance. That arrangement exists for a reason: the Lean process is not something a browser can talk to directly, so the relay is the network hop that carries messages. The backend documentation is a single file, `doc/DOCUMENTATION.md`, and the README says it describes the server part, meaning the contents of `server/` and `relay/`.

The Lean side is compiled with the Lean toolchain rather than npm. The build script for the server changes into `server` and calls `lake build`, and the test build does the same inside `cypress/TestGame`, so there is a small Lean project used as a test fixture. That means two toolchains are involved in a full build: the Node one for the client and relay, and Lean for the game server and the test game.

Other root entries describe the operational surface. `ecosystem.config.cjs` is a process manager configuration, `cypress.config.ts` and the `cypress` directory hold end to end tests, `NOTES.md` and `NOTES_SUBDOMAIN.md` look like running notes, and `TODO-skipped-commits.txt` is an explicit list of commits that were skipped. There is also a `.vscode` directory and a `tsconfig.json` for the TypeScript side, and the client depends on `jotai-family` for state and `tailwind-merge` for class name handling.

Running the stack from the package manifest

The manifest is the only place where the commands are written down, so it is worth reading as a build script rather than as metadata. Development mode starts three things at once, the server build, the relay and the client, each under its own name and colour.

    "start": "concurrently -n server,relay,client -c blue,yellow,green \"npm run build:server\" \"npm run start:relay\" \"npm run start:client\"",
    "start:relay": "npm --workspace relay run dev",
    "start:client": "npm --workspace client run dev",

The individual build steps are separate scripts, and the server one is a call into the Lean toolchain.

    "build": "npm run build:server && npm run build:relay && npm run build:client && npm run build:test",
    "build:server": "cd server && lake build",
    "build:client": "npm --workspace client run build",
    "build:relay": "npm --workspace relay run build",
    "build:test": "cd cypress/TestGame && lake build",

So the practical first run is: install the npm dependencies, make sure a Lean toolchain with `lake` on the path is available, then trigger the start script. What you should see is three named processes running, with the client in the workspace development mode and the relay starting alongside the compiled server.

Tests exist and they drive the whole stack. The test script builds the fixture game first and then runs the server and Cypress together, and a separate production variant builds everything and points the relay at a port.

    "test": "npm run build:test && concurrently -n server,cypress -c blue,green \"npm start\" \"cypress run\" -k -s first --hide server",
    "test:prod": "npm run build && concurrently -n server,cypress -c blue,green \"PORT=3000 npm run production\" \"cypress run\" -k -s first"

There is also a `translate` script in the client workspace, which lines up with the project's invitation to translate the interface.

The bubblewrap boundary around the Lean instance

The security section of the README is short and unusually direct. Giving users access to a Lean instance running on the server is described as a severe security risk, and the reason is that a Lean instance executes code. The mitigation is that the Lean server is started with bubblewrap, a sandbox that restricts what the process can see and do on the host.

That single decision shapes the rest of the architecture. It is the reason the Lean process cannot simply be exposed to the browser, the reason there is a relay in the middle, and the reason hosting your own instance is a documented task rather than a casual deployment. Any page of the site that runs player supplied or player modified Lean code is running inside that boundary.

For an operator, bubblewrap is a dependency with real consequences. It is not a general container runtime, so the way the server invokes it and what it grants become part of your security boundary, and the hosting document is where those details belong. The project does not publish a hardening checklist in the README, so the operational questions about sandbox configuration, resource limits and what happens if a player submits code that tries to escape have to be answered from the server code and the hosting guide.

One thing the README does spell out is the outage path. If adam.math.hhu.de is down, the maintainers ask for an issue to be opened or an email to the listed address, and they distinguish that from bug reports and feature requests about the game interface, which go to the issues page of this repository. Specific bugs in a particular game are directed to that game's own repository or to its maintainer.

The document chain for creating, publishing and updating a game

The documentation is organised as a sequence of steps, and the README points at the ones that usually cause trouble. The main document to consult is `doc/create_game.md`. The others are `doc/hints.md` for the `Hint` and `Branch` tactics, `doc/running_locally.md` for playing on your own machine, `doc/update_game.md` for moving an existing game to a new Lean version, `doc/publish_game.md` for loading a game onto the server for others to play, and `doc/troubleshoot.md`.

That sequence is the actual workflow for a maintainer, and it exposes the main ongoing cost of using this project. A Lean game is Lean source code, and Lean source code is coupled to a compiler version. When the Lean toolchain moves, an existing game can stop compiling, which is exactly what `doc/update_game.md` exists for. Published games are therefore not a one time upload: they carry a maintenance obligation tied to the pace of Lean releases.

The hosting guide `doc/hosting.md` is described as how to set up your own Lean Game Server, and `doc/development.md` holds the development instructions for people working on the codebase itself. Contributors are explicitly welcome.

The honest caveat is stated in the README as well: the documentation is very much work in progress, and the links are expected to be up to date even if the prose is not complete. For a game author that means the tutorial is the authority on the workflow, and the tutorial is a document in the repository rather than a polished manual.

What is missing: releases, a stable docs set, and a deployment story

Three gaps are worth naming before an engineer adopts this. The first is that the repository has no GitHub releases at all. There is no versioned artefact to pin, no changelog, and no upgrade notes to read. The project is versioned internally in the manifest, where the name is `lean4game` and the version field reads `0.1.0`, and the manifest is marked private, which is consistent with a server application that is deployed from source rather than consumed as a package.

The second gap is the documentation, which describes itself as work in progress. Every step a game author needs exists as a file, but the README warns that the wording may lag. There is also no published guide in the README to the exact Node and Lean versions expected, no changelog for the frontend, and no migration notes beyond the single `doc/update_game.md` page.

The third gap is deployment. The manifest offers a `production` script that delegates to the relay workspace, and the process manager configuration file suggests a process manager is expected, but the README does not give a deployment recipe for a public instance. The hosting document is the place to look, and it is not quoted in the README.

The licence is GPL-3.0, which is a heavier obligation than a permissive licence and needs its own review before you fork the server and change it. For a service that plays public puzzle games, the copyleft question is mostly about whether you publish modifications to the server itself. That is a legal read of the licence terms and not advice, but it is the kind of thing to settle with whoever owns the code in your organisation.

The project has been active, with the last push to the tree on 2026-10-20, and the README credits Alexander Bentkamp and Jon Eugster as the primary developers, with contributions from the game maintainers listed in the contact table.

Where lean4game sits against the Lean Game Maker and NNG

The credits section names the ancestry, which is the best available comparison. The project is based on ideas from the Lean Game Maker, from the Natural Number Game by Kevin Buzzard and Mohammad Pedramfar, and on a prototype called NNG4 by Patrick Massot. The people behind those efforts also appear in the contact table as maintainers of individual games, including the Natural Number Game itself.

The difference is the layer that was added. The earlier work was about games as Lean artefacts, and the ideas it contributed are the game design and the Lean side of the experience. lean4game is the hosted platform around them, and the repository root shows what that platform costs: a React client, a relay, a sandboxed server process, a process manager configuration, a Cypress end to end test suite and a set of Lean test fixtures.

So the choice is not really between two ways of writing a game. It is between running a game as Lean code that learners check on their own machines, and running a platform that serves games over HTTP, tracks hints and branches, supports translated interfaces and can be self hosted. For a single course exercise, the platform is more than you need. For a collection of exercises offered to an audience, the platform is the part that is genuinely hard to build, and the relay plus bubblewrap design is the concrete answer to it.

Editorial conclusion

Adopt lean4game if you are writing Lean 4 exercises and want learners to solve them in a browser with hints and branch tracking, or if you want to run your own instance instead of relying on adam.math.hhu.de. Do not adopt it if you need a packaged deployment, a published release trail, or documentation that covers every operational detail, because the repository ships no GitHub releases and its own documentation is described as work in progress. Before committing, read `doc/hosting.md` and `doc/DOCUMENTATION.md`, then confirm that the Lean instance runs inside bubblewrap on your target machine and that you can rebuild a published game after a Lean version change, following `doc/update_game.md`.

Frequently asked questions

Official sources

1. Issues
2. leanprover-community/lean4game on GitHub
3. License: GPL-3.0
4. Project website
5. README