diff --git a/.gitignore b/.gitignore
index b182198..a05d3c5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,6 @@ lake-packages/
 **/.DS_Store
 .i18n/**/*.mo
 *~
+
+# Nix flake build artifacts
+.lean4game-nix/
diff --git a/FLAKE_USAGE.md b/FLAKE_USAGE.md
new file mode 100644
index 0000000..a22b644
--- /dev/null
+++ b/FLAKE_USAGE.md
@@ -0,0 +1,313 @@
+# Nix Flake Usage for NNG4
+
+This flake provides a complete development and runtime environment for the Lean4 Natural Number Game without requiring Docker or VSCode.
+
+## Quick Start
+
+The fastest way to get started:
+
+```bash
+nix run
+```
+
+This single command will:
+1. Set up the lean4game platform in `.lean4game-nix/`
+2. Install all npm dependencies
+3. Build the Lean game (if needed)
+4. Start the game server at `http://localhost:3000`
+
+**First run takes 5-15 minutes** due to dependency downloads and Lean compilation. Subsequent runs are much faster.
+
+## Available Commands
+
+### `nix run` - Start the Game Server
+
+Starts the complete game server with web interface:
+
+```bash
+nix run
+```
+
+The game will be available at: **http://localhost:3000/#/g/local/NNG4**
+
+Press `Ctrl+C` to stop the server.
+
+### `nix develop` - Development Shell
+
+Enter a development environment with all tools available:
+
+```bash
+nix develop
+```
+
+This provides:
+- `elan` - Lean toolchain manager
+- `lake` - Lean build tool
+- `node` and `npm` (Node.js 20)
+- Helper scripts (see below)
+
+### `nix build` - Build the Game
+
+Build the Lean game and create a `./result` symlink:
+
+```bash
+nix build
+```
+
+The compiled game will be in `./result/`.
+
+## Helper Scripts
+
+When inside `nix develop`, additional commands are available:
+
+### `setup-nng4-workspace`
+
+Sets up the workspace for the first time:
+
+```bash
+setup-nng4-workspace
+```
+
+This script:
+1. Copies lean4game to `.lean4game-nix/`
+2. Installs npm dependencies
+3. Updates Lake dependencies
+4. Fetches mathlib cache (speeds up compilation significantly)
+5. Builds the game with `lake build`
+
+**Note:** Only needed if you want to manually set up before running the server.
+
+### `run-nng4-server`
+
+Starts the game server:
+
+```bash
+run-nng4-server
+```
+
+Same as `nix run` but from within the dev shell.
+
+## Directory Structure
+
+The flake sets up the following structure:
+
+```
+NNG4/                          # Your game repository
+├── flake.nix                  # Nix flake configuration
+├── flake.lock                 # Locked dependency versions
+├── .lean4game-nix/            # lean4game platform (created by setup)
+│   ├── client/                # React frontend
+│   ├── relay/                 # Node.js relay server
+│   ├── server/                # Lean GameServer
+│   └── node_modules/          # npm dependencies
+├── Game/                      # Your game source code
+├── lakefile.lean              # Lake build configuration
+└── lean-toolchain             # Lean version (v4.23.0)
+```
+
+## How It Works
+
+The flake:
+
+1. **Fetches lean4game** at the matching version (v4.23.0) from GitHub
+2. **Creates a development shell** with:
+   - Lean 4.23.0 via elan
+   - Node.js 20
+   - Build tools (git, curl, etc.)
+3. **Sets up the workspace** by:
+   - Copying lean4game to `.lean4game-nix/` (sibling structure)
+   - Installing npm dependencies
+   - Building your game with Lake
+4. **Runs the server** with:
+   - Environment variables for single-game mode
+   - Relay server on port 8080
+   - Vite dev server on port 3000
+   - Lean server for proof verification
+
+## Workflow Examples
+
+### Daily Development
+
+1. Make changes to your game code in `Game/`
+2. Rebuild: `nix develop -c lake build`
+3. Restart server: `nix run`
+4. View changes at `http://localhost:3000/#/g/local/NNG4`
+
+### Starting from Scratch
+
+If you clone this repository fresh:
+
+```bash
+# One command does it all:
+nix run
+
+# Or step by step:
+nix develop
+setup-nng4-workspace
+run-nng4-server
+```
+
+### Clean Rebuild
+
+To force a complete rebuild:
+
+```bash
+nix develop
+lake clean
+lake build
+run-nng4-server
+```
+
+### Remove Build Artifacts
+
+```bash
+# Remove the lean4game platform
+rm -rf .lean4game-nix/
+
+# Remove Lean build artifacts
+lake clean
+
+# Next nix run will rebuild everything
+```
+
+## Troubleshooting
+
+### "npm install" takes forever
+
+This is normal on first run. The lean4game platform has 1600+ npm packages. Subsequent runs reuse the installed packages.
+
+### Mathlib builds are slow
+
+On first build, run this to fetch prebuilt mathlib:
+
+```bash
+nix develop
+lake exe cache get
+lake build
+```
+
+### Port 3000 or 8080 already in use
+
+Stop any other processes using these ports:
+
+```bash
+lsof -ti:3000 | xargs kill -9
+lsof -ti:8080 | xargs kill -9
+```
+
+### Changes to game code not reflected
+
+Rebuild the game:
+
+```bash
+nix develop -c lake build
+```
+
+Then reload the browser (hard refresh: `Ctrl+Shift+R`).
+
+### "Git tree is dirty" warning
+
+This is harmless. Nix warns when the git repository has uncommitted changes. The flake still works correctly.
+
+## Technical Details
+
+### Version Pinning
+
+- **Lean:** 4.23.0 (from `lean-toolchain`)
+- **lean4game:** v4.23.0 tag (from GitHub)
+- **Node.js:** 20.x (matching Dockerfile)
+- **npm packages:** Locked in lean4game's `package-lock.json`
+
+### Why `.lean4game-nix/`?
+
+The lean4game platform expects to be a sibling directory to your game. Since Nix works with immutable store paths, we copy it to a local directory that can be modified (for npm install, etc.).
+
+### Differences from Docker Setup
+
+**Docker approach:**
+- Uses containers with Ubuntu base
+- Requires Docker daemon
+- Builds image with all dependencies
+- Mounts volumes for development
+
+**Nix approach:**
+- Uses Nix store for dependencies
+- No daemon needed
+- Declarative, reproducible environment
+- Direct file access, no volumes
+
+Both produce the same result: a working game server at `http://localhost:3000`.
+
+## Advanced Usage
+
+### Update lean4game Version
+
+To update lean4game to a newer version:
+
+1. Edit `flake.nix`:
+   ```nix
+   lean4game = {
+     url = "github:leanprover-community/lean4game/v4.XX.0";  # Change version
+     flake = false;
+   };
+   ```
+
+2. Update the lock file:
+   ```bash
+   nix flake update lean4game
+   ```
+
+3. Rebuild:
+   ```bash
+   rm -rf .lean4game-nix/
+   nix run
+   ```
+
+### Use Local lean4game Clone
+
+If you want to develop lean4game itself, you can point to a local clone:
+
+1. Clone lean4game:
+   ```bash
+   cd ..
+   git clone https://github.com/leanprover-community/lean4game.git
+   ```
+
+2. Edit `flake.nix`:
+   ```nix
+   lean4game = {
+     url = "path:../lean4game";  # Local path
+     flake = false;
+   };
+   ```
+
+3. Rebuild:
+   ```bash
+   nix flake lock --update-input lean4game
+   nix run
+   ```
+
+### Multi-System Support
+
+The flake supports:
+- `x86_64-linux` (tested)
+- `aarch64-linux`
+- `x86_64-darwin` (macOS Intel)
+- `aarch64-darwin` (macOS Apple Silicon)
+
+All platforms should work identically.
+
+## Contributing
+
+When contributing changes:
+
+1. **Keep flake.nix in sync** with the Lean version in `lean-toolchain`
+2. **Commit flake.lock** to ensure reproducible builds
+3. **Test with** `nix flake check` before committing
+
+## Resources
+
+- [Nix Flakes Manual](https://nixos.org/manual/nix/stable/command-ref/new-cli/nix3-flake.html)
+- [lean4game Documentation](https://github.com/leanprover-community/lean4game)
+- [NNG4 README](./README.md)
+- [Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)
diff --git a/README.md b/README.md
index bf6d97f..30a38b5 100644
--- a/README.md
+++ b/README.md
@@ -13,6 +13,16 @@ You can develop the game as any lean project and use `lake build` to build it.
 Moreover, there are multiple ways to run the game while developing it, which are described in
 [Running Games Locally](https://github.com/leanprover-community/lean4game/blob/main/doc/running_locally.md)
 
+### Nix Flake
+
+If you use Nix, you can run the game locally without Docker or VSCode:
+
+```bash
+nix run    # Start the game server at http://localhost:3000
+```
+
+See [FLAKE_USAGE.md](./FLAKE_USAGE.md) for complete documentation.
+
 ## Contributing
 
 PRs/Issues fixing typos, inconsistencies, missing hints, etc. are very welcome!
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..e035929
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,79 @@
+{
+  "nodes": {
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1731533236,
+        "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "lean4game": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1758355902,
+        "narHash": "sha256-SPgCAddEXtHhXC8AqkLw+MwwCr8186Sot5k4ePxu0mQ=",
+        "owner": "leanprover-community",
+        "repo": "lean4game",
+        "rev": "36aa0824532ba3a3788d6d2e7cf72905e891cf14",
+        "type": "github"
+      },
+      "original": {
+        "owner": "leanprover-community",
+        "ref": "v4.23.0",
+        "repo": "lean4game",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1762596750,
+        "narHash": "sha256-rXXuz51Bq7DHBlfIjN7jO8Bu3du5TV+3DSADBX7/9YQ=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "b6a8526db03f735b89dd5ff348f53f752e7ddc8e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "lean4game": "lean4game",
+        "nixpkgs": "nixpkgs"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..52e1437
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,213 @@
+{
+  description = "Lean4 Natural Number Game - Development Environment";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+    flake-utils.url = "github:numtide/flake-utils";
+
+    # Fetch lean4game at the matching version
+    lean4game = {
+      url = "github:leanprover-community/lean4game/v4.23.0";
+      flake = false;
+    };
+  };
+
+  outputs = { self, nixpkgs, flake-utils, lean4game }:
+    flake-utils.lib.eachDefaultSystem (system:
+      let
+        pkgs = nixpkgs.legacyPackages.${system};
+
+        # Node.js 20 to match Docker setup
+        nodejs = pkgs.nodejs_20;
+
+        # Lean toolchain (we'll use elan to manage it)
+        elan = pkgs.elan;
+
+        # Helper script to set up the workspace
+        setupWorkspace = pkgs.writeShellScriptBin "setup-nng4-workspace" ''
+          set -e
+
+          WORKSPACE_ROOT="$(pwd)"
+          GAME_DIR="$WORKSPACE_ROOT"
+          LEAN4GAME_DIR="$WORKSPACE_ROOT/.lean4game-nix"
+
+          echo "Setting up NNG4 workspace..."
+
+          # Create lean4game directory if it doesn't exist
+          if [ ! -d "$LEAN4GAME_DIR" ]; then
+            echo "Copying lean4game to $LEAN4GAME_DIR..."
+            cp -r ${lean4game} "$LEAN4GAME_DIR"
+            chmod -R u+w "$LEAN4GAME_DIR"
+          fi
+
+          # Install npm dependencies in lean4game
+          if [ ! -d "$LEAN4GAME_DIR/node_modules" ]; then
+            echo "Installing npm dependencies in lean4game..."
+            cd "$LEAN4GAME_DIR"
+            npm install
+          fi
+
+          # Set up Lean toolchain
+          cd "$GAME_DIR"
+          if [ ! -d ".lake" ]; then
+            echo "Setting up Lean dependencies..."
+            echo "This may take a while on first run..."
+
+            # Update Lake dependencies
+            lake update -R
+
+            # Fetch mathlib cache (speeds up build significantly)
+            echo "Fetching mathlib cache..."
+            lake exe cache get || echo "Warning: Failed to fetch cache, build will be slower"
+
+            # Build the game
+            echo "Building the game..."
+            lake build
+          else
+            echo "Lake dependencies already set up. Run 'lake clean && lake build' to rebuild."
+          fi
+
+          echo ""
+          echo "✓ Workspace setup complete!"
+          echo ""
+          echo "To start the game server, run:"
+          echo "  nix run"
+          echo ""
+          echo "Or manually:"
+          echo "  cd .lean4game-nix && npm start"
+        '';
+
+        # Script to run the game server
+        runGameServer = pkgs.writeShellScriptBin "run-nng4-server" ''
+          set -e
+
+          WORKSPACE_ROOT="$(pwd)"
+          GAME_DIR="$WORKSPACE_ROOT"
+          LEAN4GAME_DIR="$WORKSPACE_ROOT/.lean4game-nix"
+
+          # Ensure workspace is set up
+          if [ ! -d "$LEAN4GAME_DIR/node_modules" ]; then
+            echo "Workspace not set up. Running setup..."
+            setup-nng4-workspace
+          fi
+
+          # Get the game name from the directory
+          GAME_NAME=$(basename "$GAME_DIR")
+
+          echo "Starting NNG4 game server..."
+          echo "Game: $GAME_NAME"
+          echo ""
+
+          cd "$LEAN4GAME_DIR"
+
+          # Set environment variables for single-game mode
+          export VITE_LEAN4GAME_SINGLE=true
+          export VITE_LEAN4GAME_SINGLE_NAME="$GAME_NAME"
+          export NODE_ENV=development
+
+          # Start the server
+          echo "Server will be available at: http://localhost:3000/#/g/local/$GAME_NAME"
+          echo ""
+          npm start
+        '';
+
+        # Build derivation for the game
+        buildGame = pkgs.stdenv.mkDerivation {
+          pname = "nng4";
+          version = "4.23.0";
+
+          src = ./.;
+
+          nativeBuildInputs = [
+            elan
+            pkgs.git
+            pkgs.curl
+          ];
+
+          buildPhase = ''
+            # Set up elan home
+            export ELAN_HOME=$TMPDIR/elan
+            export PATH="$ELAN_HOME/bin:$PATH"
+
+            # Lake will read the lean-toolchain file
+            lake update -R
+
+            # Try to fetch cache (may fail, that's ok)
+            lake exe cache get || echo "Cache fetch failed, continuing..."
+
+            # Build the game
+            lake build
+          '';
+
+          installPhase = ''
+            mkdir -p $out
+            cp -r .lake $out/
+            cp -r Game $out/
+            cp Game.lean $out/
+            cp lakefile.lean $out/
+            cp lean-toolchain $out/
+          '';
+        };
+
+      in {
+        # Development shell with all tools
+        devShells.default = pkgs.mkShell {
+          buildInputs = [
+            # Lean toolchain
+            elan
+
+            # Node.js and npm
+            nodejs
+
+            # Build tools
+            pkgs.git
+            pkgs.curl
+            pkgs.cacert
+
+            # Helper scripts
+            setupWorkspace
+            runGameServer
+          ];
+
+          shellHook = ''
+            echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
+            echo "  Lean4 Natural Number Game - Development Environment"
+            echo "━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━"
+            echo ""
+            echo "Available commands:"
+            echo "  setup-nng4-workspace  - Set up lean4game and build the game"
+            echo "  run-nng4-server       - Start the game server"
+            echo "  lake                  - Lean build tool"
+            echo "  elan                  - Lean toolchain manager"
+            echo ""
+            echo "Quick start:"
+            echo "  1. setup-nng4-workspace  (first time only, ~5-15 min)"
+            echo "  2. run-nng4-server       (start the game)"
+            echo ""
+            echo "Or use:"
+            echo "  nix run                  (does both steps)"
+            echo ""
+
+            # Set up elan environment
+            export ELAN_HOME="$HOME/.elan"
+            export PATH="$ELAN_HOME/bin:$PATH"
+
+            # Ensure elan is initialized
+            if [ ! -d "$ELAN_HOME" ]; then
+              echo "Initializing elan..."
+              elan default stable
+            fi
+          '';
+        };
+
+        # Default package - builds the game
+        packages.default = buildGame;
+
+        # Run app - starts the game server
+        apps.default = {
+          type = "app";
+          program = "${runGameServer}/bin/run-nng4-server";
+        };
+      }
+    );
+}