Home / Roadmap

Roadmap

Where we are, where we're going. This is a living document.

Phase 1 — Static Proof Gym (now)

A static site with lessons and exercises. You copy Lean 4 code into Lean 4 Web or your local VS Code to check proofs. Low friction, zero infrastructure.

• Done: Logic track (6 exercises)
• Done: Natural Numbers track (5 exercises)
• Next: Sets track
• Next: Functions track
• Next: More exercises per track

Phase 2 — Embedded Editor

Embed a Lean 4 code editor directly in each exercise page. Type your proof, see feedback inline. No copy-pasting needed.

Based on lean4web — a Monaco editor frontend that talks to a Lean 4 language server via WebSocket. Requires hosting a Lean server (Docker + Nginx + pm2).

• Self-host lean4web on Hetzner (cx23, 2 vCPU, 4GB)
• Embed editor iframe in exercise pages
• Pre-populate with exercise skeleton code
• Syntax highlighting, error messages, goal state visible

Phase 3 — Game Engine

Full integration with lean4game — the engine behind the Natural Number Game. Structured levels, tactic introduction, guided proof construction.

• Write exercises as Lean 4 game levels
• Tactic panel shows available tactics per level
• Goal state updates live as you type
• Bubblewrap sandboxing for security
• ~20 concurrent users per server node

Phase 4 — Community

Progress tracking, user accounts, community-contributed exercises, difficulty ratings, solution discussions.

• User accounts with proof history
• Community exercise submissions
• Difficulty voting (like Project Euler)
• Solution discussions (after you've proved it)
• Track completion badges

Architecture

Phase 1 (now):
  Static HTML/CSS on Cloudflare Pages
  User copies code to Lean 4 Web or local VS Code

Phase 2:
  Cloudflare Pages (frontend)
    |
    | WebSocket
    v
  Hetzner cx23 (lean4web server)
    - Docker: Lean 4 + Mathlib
    - Nginx reverse proxy
    - pm2 process manager

Phase 3:
  Cloudflare Pages (frontend)
    |
    | WebSocket
    v
  Hetzner (lean4game server)
    - Node.js relay server
    - Lean 4 gameserver binary
    - Bubblewrap sandbox per user
    - ~20 concurrent users per node

Tracks Plan

1. Logic          ████████████ done (6 exercises)
2. Numbers        ████████████ done (5 exercises)
3. Sets           ░░░░░░░░░░░░ planned
4. Functions      ░░░░░░░░░░░░ planned
5. Algebra        ░░░░░░░░░░░░ planned
6. Real Analysis  ░░░░░░░░░░░░ planned
7. Topology       ░░░░░░░░░░░░ future
8. Combinatorics  ░░░░░░░░░░░░ future
9. Number Theory  ░░░░░░░░░░░░ future