Senior Engineer Simulator: The Data Center

Status: SEV-1 Incident Role: Senior Site Reliability Engineer (You) Directives: Formally verify critical infrastructure to prevent data loss.

Play the Game Here

---

📋 Overview

Senior Engineer Simulator (originally "Logic for Engineers") is a Lean 4 game that gamifies formal verification. Instead of proving abstract mathematical theorems, you are tasked with verifying "Jira Tickets" to prevent bugs in a critical production system.

The game bridges the gap between software engineering intuition and mathematical proof, demonstrating how functional programming concepts (Maps, Folds, Recursion) can be rigorously verified.

🏗️ Architecture

This project is built using the Lean 4 Game Engine.

• Language: Lean 4 (Functional programming + Theorem Proving)
• Engine: lean4game (Web frontend + Server-side Lean execution)
• Structure:
  • Game/Levels/: Contains the actual game content.
  • Game/Levels/TheDataCenter.lean: The core "World" defining the narrative and importing levels.
  • Game.lean: The entry point configuration.

The "Data Center" World

The game introduces a custom world, "The Data Center", designed to teach structural induction on Lists.

• Level 1 (Ticket-1041): my_map id L = L (Identity Verification)
• Level 2 (Ticket-1042): length (my_map f L) = length L (Buffer Overflow Prevention)
• Level 3 (Ticket-1043): length (my_append L1 L2) = total_length (Merge Logic)
• Level 4 (Ticket-1044): map (g ∘ f) = map g ∘ map f (Compiler Optimization)
• Level 5 (Ticket-1045): length (my_reverse L) = length L (Backup Integrity)

---

🚀 Setup Steps

To run or modify this game locally:

Prerequisites

1. Install Lean 4: Follow the Generic Installation Instructions.
2. VS Code: Install the "Lean 4" extension.

Running Locally

1. Clone the Repo:

   git clone https://github.com/adam0white/lean-experiments.git
   cd lean-experiments

2. Build the Game:

   lake build

   Note: This downloads dependencies and compiles the math library. It may take a few minutes.
3. Start the Server: Run the generic "Start Game" task in VS Code, or:

   lake exe game_server

   Then open the local URL provided (usually localhost:3000 or similar depending on the frontend setup).

---

🔄 What We Changed (Refactoring Log)

We reframed the original "Logic Game" template into a cohesive engineering simulation.

1. Narrative Overhaul

• From: Abstract "Induction" and "Logic" levels.
• To: "SEV-1 Incident Response". Levels are now "Jira Tickets" (e.g., Ticket-1042: Buffer Overflow Check).
• Why: To make formal verification relatable to software engineers.

2. New World: "The Data Center"

• Created a 5-level progression system focusing on List Induction.
• Introduced custom definitions (my_map, my_append, my_reverse) to avoid trivializing proofs with standard library lemmas.
• Engineered a smooth difficulty curve:
  • L1-L2: Basic structural induction.
  • L3: Induction with arithmetic lemmas (Nat.add_assoc).
  • L4: Higher-order function optimization (map fusion).
  • L5: Complex induction reusing previous lemmas (append_length).

3. Engineering-First Features

• Hidden Hints: Hints are enabled but hidden by default (Hint (hidden := true)), simulating the experience of "consulting documentation" only when stuck.
• Production-Ready Proofs: The proofs emphasize readability and maintainability (using simp, rw with named hypotheses like tail_ih).

---

🛠️ Contributing

PRs are welcome! If you want to add a new "Ticket" (Level), please follow the Ticket-XXXX naming convention and ensure it fits the "Data Center" theme.

License: Apache 2.0