ZK certificate #3
Probă: comutativitatea adunării pe Nat — chitanță succintă RISC Zero (program lean_check, RTX 4090)
✅ verified mathematically: the receipt proves the Lean kernel (nanoda, in the zkVM) accepted a proof
This certificate is not bound to a challenge: it proves a proof of the statements below exists, and you compare them with the problem yourself. Certificates made with the sealed comparator (journal v2) also prove the statements are exactly a challenge's.
Statements proven (the proofs stay secret)
- Eq.symm
theorem Eq.symm.{u} : forall {α : Sort u} {a b : α}, Eq a b → Eq b a := _ - congrArg
theorem congrArg.{u v} : forall {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), Eq a₁ a₂ → Eq (f a₁) (f a₂) := _ - Nat.zero_add
theorem Nat.zero_add (n : Nat) : Eq (HAdd.hAdd (OfNat.ofNat 0) n) n := _
- Nat.succ_add
theorem Nat.succ_add (n m : Nat) : Eq (HAdd.hAdd (Nat.succ n) m) (Nat.succ (HAdd.hAdd n m)) := _
- Nat.add_comm
theorem Nat.add_comm (n m : Nat) : Eq (HAdd.hAdd n m) (HAdd.hAdd m n) := _
- add_comm'
theorem add_comm' (n m : Nat) : Eq (HAdd.hAdd n m) (HAdd.hAdd m n) := _
- Holder
- u_XI6mv-HHRwyD
The holder is the account that posted the receipt. The receipt itself is not yet bound to an account or a transaction: it proves that a proof exists, not who owns it. - Recorded at (UTC)
- 2026-09-17T13:57:40.322020Z
- Program image id (lean_check)
- b80838fed027ffe2c75c05c45e46d8f2a3385fcb2ac4564084a732a53a4ef99f
- Axiom policy (axioms the checker was allowed to accept)
- Classical.choice, Lean.trustCompiler, Quot.sound, propext
- ⚠ This certificate's policy also allows Lean.trustCompiler, the axiom behind native_decide: it trusts the whole Lean compiler, not only the kernel. New certificates do not allow it.
- SHA-256 of the (secret) export
- b4279761d83e88a2737beead8ed1bc6d742498310eaeb46f502dab2a8c8c08bd · 53 declarations checked
- receipt
- succinct · sha256 9d7abf96499c5c46e9c3a3f3a5aba27220be2b340c5dc87753720fc0b8eb1bc9 · Download the receipt
- Entry hash
- 4d48736c3bf88e5994e55f5a401f21ea2198ef5ab7d0f05dc13955522a46f33d · #3
Verify it yourself
Build the verifier from zk/lean_check/verifier (Rust), then run it on the receipt with the image id. The image id is the hash of the fixed program; anyone rebuilding zk/lean_check obtains the same id.
lean_check_verifier receipt.bin b80838fed027ffe2c75c05c45e46d8f2a3385fcb2ac4564084a732a53a4ef99f