Nasrudin starts from mathematical axioms and physics postulates, then evolves new theorems with a genetic algorithm — formally proving every survivor in Lean 4. Eventually, it rediscovers known physics. On its own.
Workers run the full Rust GA + Lean 4 prover locally and only upload theorems they've already verified. The central server then re-verifies every submission with its own Lean instance before accepting it. Double-verification, no trust.
Mutate. Crossover. Compose. Verify. Five generations from the Lagrangian seed to F = ma, all of it formal.
Some of these were rediscovered without supervision. Others are search targets we're patiently waiting for. Each carries the GA cycle it emerged from and a re-runnable Lean proof.
Loading featured discoveries from corpus...
Loading featured discoveries from corpus...
Loading featured discoveries from corpus...
Loading featured discoveries from corpus...
Loading featured discoveries from corpus...
Loading featured discoveries from corpus...
Anyone can run a worker. Each generates and verifies theorems locally, then POSTs discoveries to the central server, which re-verifies before accepting. The server is the gatekeeper, not the oracle.
Two steps. One command. Your machine starts mutating axioms in minutes — the installer detects your platform, fetches the right binary, and starts the worker. Every theorem it verifies and the server accepts gets your pseudonym attached, forever.
Sign in, then open /api-keys → "+ New key" → Kind: Worker. Copy the nsk_worker_… value.
curl -fsSL https://nasrudin.org/install.sh | NASRUDIN_WORKER_KEY=nsk_worker_… bash
One command. The script detects your platform, installs the Lean toolchain if it isn't already there, downloads the matching binary from this repo's latest release, verifies its SHA-256, and starts the worker.
First run warms the Mathlib cache (a few minutes); subsequent runs reuse it. Ctrl+C is clean.