ZK certificates: “I have a proof”
A receipt from the fixed program lean_check shows that one Lean kernel (nanoda, running inside the RISC Zero zkVM) accepted a proof of the statements below. The proof is not published: not here, not in the receipt. The receipt is designed to reveal nothing about it; RISC Zero targets zero-knowledge but has not yet published a formal proof of that property. We verify each receipt against the program's image id; anyone can repeat the verification with the public verifier.
Post a ZK certificate · Public verifications of Lean solutions
Program image id (lean_check): 9eb59152d4c880edce28e437b688d6fc84be75ed66e2e36ec8d5987a288acc84, 3cd17b93d194a6bef13c753823a36c43ad155ff36e1f9402e396ab3344c464b4, b80838fed027ffe2c75c05c45e46d8f2a3385fcb2ac4564084a732a53a4ef99f, 9eb59152d4c880edce28e437b688d6fc84be75ed66e2e36ec8d5987a288acc84
| # | Recorded at (UTC) | Statements proven (the proofs stay secret) | receipt |
|---|---|---|---|
| #7 | 2026-09-25T21:03:40 | add_comm' — Sealed comparator (v2): bound to this problem's challenge — proof kept by the house, made on a rented A5000 in 109 s | succinct · 🔒 |
| #3 | 2026-09-17T13:57:40 | Eq.symm, congrArg, Nat.zero_add … — Probă: comutativitatea adunării pe Nat — chitanță succintă RISC Zero (program lean_check, RTX 4090) | succinct |