Certificate ZK: „am o demonstrație”
O chitanță produsă de programul fix lean_check arată că un nucleu Lean (nanoda, rulat în mașina virtuală RISC Zero) a acceptat o demonstrație a enunțurilor de mai jos. Demonstrația nu e publicată: nici aici, nici în chitanță. Chitanța e proiectată să nu dezvăluie nimic despre ea; RISC Zero urmărește proprietatea de fără-dezvăluire, dar n-a publicat încă o demonstrație formală a ei. Verificăm fiecare chitanță contra id-ului de imagine al programului; oricine poate repeta verificarea cu verificatorul public.
Postează un certificat ZK · Verificări publice ale soluțiilor Lean
Id-ul de imagine al programului (lean_check): 9eb59152d4c880edce28e437b688d6fc84be75ed66e2e36ec8d5987a288acc84, 3cd17b93d194a6bef13c753823a36c43ad155ff36e1f9402e396ab3344c464b4, b80838fed027ffe2c75c05c45e46d8f2a3385fcb2ac4564084a732a53a4ef99f, 9eb59152d4c880edce28e437b688d6fc84be75ed66e2e36ec8d5987a288acc84
| # | Înscris la (UTC) | Enunțuri demonstrate (demonstrațiile rămân secrete) | chitanță |
|---|---|---|---|
| #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 |