NasrudinSynthetic theorem · Lean 4
— workers online·— verified in 24h
Distributed theorem-generation engine · v0.4

Derive physics from pure logic.

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.

"Once, looking for a lost key under a lamppost, Nasrudin was asked why he searched there. Because the light is better here."
— a Sufi parable. We point the lamp where Lean can prove.
Run a worker node →Browse the verified corpus
0
Axioms
0
Max generation
0
Workers · live
0
Verified theorems
Live · just verified
thm:… waiting for live events…
—
 
connecting…
Livewaiting for live events…
Every proof is reproducible — download the .lean file and re-run lake build on your own machine.
§ 01 / 06
The pipeline

Five stages, one rule: nothing enters the corpus that Lean 4 hasn't proved twice.

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.

01Mathematical axioms0 indexed · Mathlib + PhysLean + physics postulates
Mathematical axiom seedsaxioms
02LLM steerer + RL banditsKimi K2.6 emits intent · 4 online bandits learn the knobs
LLM steerer + reinforcement-learning banditsLLMKimi K2.6UCB1 KdirectivecomputeUCB1 + LinUCB · γ=0.7 traces · novelty bonusreward feedback
03Rust GA enginecombine · mutate · crossover
GA mutation and crossovermutatecrossover
04Candidate theoremsawaiting first worker submission
Candidate theorem stream0/day
05Lean 4 verificationgrind · simp · omega · ring · linarith
Lean 4 verificationby simp; ring; linarithQEDaccept-rate ≈ 0.0%
06RocksDB · global corpusserver re-verifies before accepting
RocksDB corpusRocksDB · 0 verified
No candidates decided in the last 24h yet — the wise fool is patient.
§ 02 / 06
Inside one cycle

One GA cycle, step by step.

Mutate. Crossover. Compose. Verify. The trace below is captured from a real worker run — each row is an operation the GA tried and what Lean said about it. When no capture exists yet, this section says so honestly instead of inventing one.

Captured trace pending
A real GA cycle will land here once the v0.1.0 worker has been captured against the live network.
§ 03 / 06
Featured rediscoveries

Physics that found itself — and physics still in the dark.

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
...
Loading...
...

Loading featured discoveries from corpus...

Discovered at
...
Status
...
○ Loading
...
Loading...
...

Loading featured discoveries from corpus...

Discovered at
...
Status
...
○ Loading
...
Loading...
...

Loading featured discoveries from corpus...

Discovered at
...
Status
...
○ Loading
...
Loading...
...

Loading featured discoveries from corpus...

Discovered at
...
Status
...
○ Loading
...
Loading...
...

Loading featured discoveries from corpus...

Discovered at
...
Status
...
○ Loading
...
Loading...
...

Loading featured discoveries from corpus...

Discovered at
...
Status
...
§ 04 / 06
The network

A distributed prover, built from home PCs and cloud nodes.

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.

Active workers · last 60s0 pins · 6 continents
Distributed worker map
Active Idle Offline
0
Workers · live
§ 05 / 06
The corpus

Every theorem. Every proof. Trust the math, not the server.

Click any row to see its full Lean 4 proof. Download the .lean file and re-verify it on your own machine with lake build. The corpus is open, browsable, and reproducible by construction.

theorem.statement contains …
IDStatementNameDomainStatus
Loading…
§ 06 / 06
Contribute compute

Run a worker. Help physics rediscover itself.

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.

  1. 1

    Get a worker key

    Sign in, then open /api-keys → "+ New key" → Kind: Worker. Copy the nsk_worker_… value.

    Open /api-keys →
  2. 2

    Paste this into your terminal

    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.

Live preview · what you'll see when it runs
~/nasrudin-worker · ./run.shReal ./run.sh — captured 2026-04-30