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.
Emerged from Lorentz invariance + conservation of momentum.
First major rediscovery. The system was 'surprised' by simplicity.
Required first introducing combinatorial counting axioms.
Closest match to date — missing complex-Hilbert structure axiom.
Awaiting Mathlib differential-geometry expansion.
Co-derived alongside three other Maxwell equations in same week.
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.
Three commands — install, register, run. Your machine starts mutating axioms in seconds. Every theorem your node verifies and the server accepts gets your pseudonym attached, forever.
A modest desktop or cloud VM is enough. The harder you push, the faster physics arrives.