One script builds the whole stack — the Lean package, the registry CLI, the benchmark harness, the Groth16 prover — and puts the tools on your PATH. That is all it does: it writes no dataset and starts no server. Install once, then pick the path below that matches what you want to do; everything deeper lives in the expanders at the bottom.
The script checks for git; installs rust (via rustup),
elan (the Lean toolchain manager), and the wasm32 compile target
if they are missing; builds everything; and links the three tools into ~/.cargo/bin.
It clones into ./satoshis-razor, and razor runs from inside that
checkout. (The demo and zk walkthrough additionally need python3.)
Read the script before you run it — you should not have to trust this page's word
about what it does. The source of everything, this site included, is
github.com/jorikschellekens/satoshis-razor.
The installer points your CLI at this registry, so the commands below publish here, from your
terminal, in seconds — no pull request, no log file to touch. Your key signs every event locally;
the private key never leaves your machine. Prefer to keep everything on your machine?
razor remote off, or --local on any single command.
Pick an open sorry on the frontier — its page shows the exact
statement a solution must prove and pre-fills the commands. Write the proof in any
.lean file under lean/Razor/ (or lean-mathlib/RazorMathlib/
for Mathlib-environment sorries); the build picks it up automatically, and the verifier finds
the declaration wherever it is defined. FLT-RED — every exponent at least 3 factors through 4
or an odd prime — is self-contained number theory and a genuinely provable first sorry on the
live board.
Want a practice round first? ./demo.sh keeps two sorries open in your clone's
local log for exactly this: prove RZR-104 or RZR-105 in lean/Razor/Sorries/Open.lean
(replace the sorry), then submit with --local — practice stays on your
machine, and the public registry never sees it.
A proposal is a problem in plain language — costless to post, no Lean required (it can even be filed straight from the browser). To make a problem solvable, formalize it: file your candidate Lean statement with a gloss (your own plain-language reading, which is what reviewers compare against the proposal), then pin the exact statement as a sorry. The backlog lists hundreds of catalogued theorems waiting for exactly this — filing the first formal statement of one is attributed, timestamped work on the log.
Formalizing a proposal someone else already formalized? Good — independent readings are the
registry's whole fidelity mechanism. Strengthen a clump by proving your statement equivalent
to an existing one: razor bridge pins the equivalence as its own sorry, and your
admitted proof of it merges the clumps.
Write a faster implementation of a challenge spec in anvil/impls/, hand-translate
it to a Lean model in lean/Razor/Anvil/, prove it refines the executable spec, then
submit and bench. Your lane appears on the leaderboards next to its
proof.
The clone already contains the live log (registry/data/events.jsonl), so there is
nothing to load: razor serve re-derives data.json from it on every
request - append an event from the CLI and every open page updates within a few seconds. To see
the scripted walkthrough with fictional participants instead, run ./demo.sh first
(and restore afterwards with git checkout registry/data/events.jsonl).
What you have after install: three commands on your PATH (linked into ~/.cargo/bin,
so a rebuild updates them in place), and two files that are the system's entire state:
It re-validates it, requires a valid signature for any registered handle, assigns it the next
position on the log, and - for proof submissions - runs the kernel check in a throwaway container
with no network before recording the verdict. It cannot forge your events, and its verdicts are
re-checkable by anyone: razor recheck --submission SUB-you replays the check on your
own machine. The public log is mirrored to
the repository on every append,
so auditors can replay it from a checkout without trusting this server.
On the public registry, commit-reveal works without --local too:
razor commit posts the hash there, and razor submit --file reveals
when you are ready. The full trust story is on the zero-knowledge page.
If you can prove a sorry from lemmas you cannot yet prove - in a Lean file, a proof with
sorry in the gaps - register the gaps as sorries and the reduction as a split. The CLI
composes the glue statement mechanically from the pinned types, so there is nothing to get subtly
wrong:
When all children and the glue are admitted, the split reads complete: the parent is
provable by composition, which in your original file is just replacing each sorry with
the admitted proof. If the plan turns out wrong, register a better split next to it - splits are
never edited, because an admitted glue is a true theorem either way.
razor account new generates an Ed25519 keypair: the public key goes on the log as your
handle's identity, the signing key stays on your machine, in ~/.config/razor/keys/ -
outside the clone, so no script or checkout surgery can touch it. Back that file up:
it signs everything you do and cannot be regenerated. From then
on every event you author is signed automatically, the CLI refuses to append events in a registered
handle's name without its key, and razor verify-log re-checks every signature on the log.
Handles without accounts can still do everything - their events are simply marked as unsigned.
Verification treats a submission as untrusted code, because Lean elaboration can run programs: the
checker runs with network access denied (sandbox-exec on macOS, bwrap on
Linux) and is killed after a time limit. Linux does not ship bwrap by default —
install it with sudo apt install bubblewrap; without it the checker warns and runs
unsandboxed.
Sorries registered with --env mathlib pin statements written with Mathlib's definitions
and are verified in the lean-mathlib/ package, which requires Mathlib v4.31.0 (matching
the pinned toolchain, so the prebuilt cache applies). Fetch it once with
./mathlib-env.sh - it is several gigabytes. Until then the registry refuses to verify
Mathlib-environment submissions and says why.
Native scores name the machine they were measured on, and a rig can be a container instead of
bare hardware: it registers a runner command, and razor bench --rig executes the
harness through it. One script builds a Linux image with the harness inside, registers it, and
measures every challenge in it — on a Mac this means real Linux scores (Docker runs containers in a
Linux virtual machine) appear on the boards next to your host's native scores: