Certificat ZK #7

Sealed comparator (v2): bound to this problem's challenge — proof kept by the house, made on a rented A5000 in 109 s

✅ verificat matematic: chitanța dovedește că nucleul Lean (nanoda, în zkVM) a acceptat o demonstrație

🔒 Legat de provocarea (comparatorul sigilat, jurnal v2): enunțurile demonstrate sunt exact ale provocării, verificat în interiorul dovezii; 686e2a073a93140c0270f14e89eb46df2f0669fdebd3353c4cbf95d66efa5150 · 32 declarații ale enunțurilor găsite identice
✓ corespunde provocării curente a problemei
Dovedit doar pentru teoremele de mai jos. Dacă problema cere mai multe rezultate decât acestea, certificatul nu le acoperă.

Enunțuri demonstrate (demonstrațiile rămân secrete)

add_comm'

theorem add_comm' (n m : Nat) : Eq (HAdd.hAdd n m) (HAdd.hAdd m n) := _

Deținător: Valaxia (casa)
Deținătorul e contul care a postat chitanța. Chitanța în sine nu e încă legată de un cont sau de o tranzacție: dovedește că există o demonstrație, nu cui îi aparține.
Probleme: Example / Exemplu: n + m = m + n in Lean 4 (no reward)
Înscris la (UTC): 2026-09-25T21:03:40.589133Z
Id-ul de imagine al programului (lean_check): 9eb59152d4c880edce28e437b688d6fc84be75ed66e2e36ec8d5987a288acc84
Politica de axiome (axiomele pe care verificatorul avea voie să le accepte): Classical.choice, Quot.sound, propext
SHA-256 al exportului (secret): 1d2f166b162fca240f8601b1028ca93addd0e8a49ed770a3ceb5459c06d16f90 · 56 declarații verificate
chitanță: succinct · sha256 cd8b8e79770b3e9c04007a9dad4b960924206c6a24401f81cdd9363067659c93 · Descarcă chitanța
Hash-ul intrării: aa2d639079f234c5716a7107887f66a03b626dbe905df0ab59a387a0ac0c0396 · #7

Verifică singur

Construiește verificatorul din zk/lean_check/verifier (Rust), apoi rulează-l pe chitanță cu id-ul de imagine. Id-ul de imagine e hash-ul programului fix; oricine reconstruiește zk/lean_check obține același id.

lean_check_verifier receipt.bin 9eb59152d4c880edce28e437b688d6fc84be75ed66e2e36ec8d5987a288acc84