Two ways to take part without publishing your work. With commit-reveal, you register a hash of your solution file now and reveal the file later; the hash proves you had the solution at the earlier time, and nobody can steal work they cannot see. With a zero-knowledge submission, you go further: you send a short cryptographic proof (a Groth16 proof, about 200 bytes) that you possess a valid solution. The registry can check this proof in milliseconds and learns nothing about the solution itself — it is never sent.
A sorry becomes zk-solvable when someone attaches a zk route to it: a verifying key for a circuit, plus a circuit-to-statement bridge establishing that satisfying the circuit means the sorry's pinned statement is true. (Distinct from a bridge sorry, which ties two candidate statements of the same problem.) There is one kind of sorry; routes are attachments, several can coexist, and a route is never edited.
A zero-knowledge circuit is a set of equations (the demo's sorting circuit has 829 of them). A valid Groth16 proof establishes one thing: the prover knows values that satisfy all of the equations. It does not reveal those values, and it cannot be forged — a tampered proof fails verification, as the demo dataset's mallory finds out.
Satisfying a set of equations only matters if the equations say the right thing. Each route
carries a circuit-to-statement bridge tying its circuit to the sorry's pinned statement. The strongest kind is a
theorem bridge, itself a kernel-checked proof. The demo dataset
(./demo.sh) shows one: Razor.Zk.network_sound, proving that any
values satisfying its sorting circuit really do describe a correctly sorted copy of the hidden
list. This approach — prove the circuit's meaning in Lean rather than trusting its author —
comes from the zkGolf project.
Three known gaps in the demo route, stated plainly. Its Lean model uses ordinary integers while the circuit uses modular arithmetic; the proof that this difference is harmless is left open (the demo files it as proposal PRP-200). The hash function used for commitments is a simplified one, fine for a demonstration but not audited for production. And the cryptographic setup was generated from a fixed, public seed so that anyone can reproduce it; a real deployment would generate it in a multi-party ceremony.
A Lean proof is data and checking it is computation, so one circuit could cover every sorry at once: a program that runs the Lean proof checker, executed inside a proving system that attests to correct execution (a zkVM). Public inputs: a hash of the pinned proof-checking environment and the sorry's statement. Private witness: the proof. An accepted proof means "someone possesses a proof the checker accepts for this exact statement" - for any sorry, with no per-sorry circuit work.
Two facts about such a route, recorded plainly. First, its bridge can never be a theorem: "the checker accepts a proof of a statement, therefore the statement is true" is Lean's own soundness, which Lean cannot prove about itself. The bridge is instead an auditable claim - the hash of the checker binary and of the environment - which is the same kind of trust every ordinary submission already places in the checker, made explicit, plus trust in the proving system itself. Second, its cost is unmeasured: proving a checker run inside a zkVM multiplies the work by a large factor, and whether a real check proves in minutes or days is a benchmark nobody here has run.
The registry records the route kind on every zk-solved sorry, so a reader always sees which trust chain admitted it: theorem (a kernel-checked bridge, like the route below) or binary-hash (the universal route, when someone builds and measures it).