Example / Exemplu: n + m = m + n in Lean 4 (no reward) p_htUYJFuD

Criterion versions · version 2 (current)

Template: Theorem verified in Lean (the statement is a Lean declaration; the proof is checked by the kernel) · Verification rung: 0b — ZK certificate (self-contained proofs)

EXAMPLE PROBLEM — no reward, no deadline. Published by the house so a newcomer can see what a problem looks like before having an account. Task: give a Lean 4 proof (v4.35.0-rc2, core library only, no Mathlib) of the formal statement below. Verification rung 0b: the solver keeps the proof and brings a zero-knowledge certificate that the fixed checker accepts it — certificate #3 in the registry is exactly such a certificate, for this very statement (see /certificates). Sealed delivery (handing the proof to the client) opens with phase 3 of the build plan; until then this page shows the criterion only. — PROBLEMĂ-EXEMPLU — fără recompensă, fără termen. Publicată de casă, ca un nou-venit să vadă cum arată o problemă înainte să aibă cont. Cerința: o demonstrație Lean 4 (v4.35.0-rc2, doar biblioteca de bază, fără Mathlib) pentru enunțul formal de mai jos. Treapta de verificare 0b: rezolvitorul păstrează demonstrația și aduce un certificat ZK că verificatorul fix o acceptă — certificatul #3 din registru e exact un astfel de certificat, pentru chiar acest enunț (vezi /certificates). Predarea sigilată (înmânarea demonstrației către client) se deschide cu faza 3 a planului de construcție; până atunci pagina arată doar criteriul.

theorem add_comm (n m : Nat) : n + m = m + n

Delimitations (what the criterion does NOT cover): Example only: no money, no custody, no arbitration. Lean 4 v4.35.0-rc2 core (no Mathlib); permitted axioms: the standard three (propext, Quot.sound, Classical.choice). A proof that simply applies Nat.add_comm from the core library is accepted — the point is the flow, not the difficulty. Compute budget: not applicable (checking a proof of this size takes milliseconds). Doar exemplu: fără bani, custodie sau arbitraj. Lean 4 v4.35.0-rc2, nucleu (fără Mathlib); axiome permise: cele trei standard (propext, Quot.sound, Classical.choice). O demonstrație care aplică pur și simplu Nat.add_comm din bibliotecă e acceptată — contează fluxul, nu dificultatea. Buget de calcul: nu se aplică (verificarea unei demonstrații de mărimea asta ia milisecunde).

Challenge (SHA-256): 686e2a073a93140c0270f14e89eb46df2f0669fdebd3353c4cbf95d66efa5150 · download the challenge export

Package hash: 8d068d1caa7ad48d4d5566672c74c38d257a9db8168c7efe1453e9877060e2e4 · #6

Signatures

• no signatures yet

ZK certificates linked to this problem

• #7 · succinct · 56 declarations checked · ✓ matches this problem's current challenge — Sealed comparator (v2): bound to this problem's challenge — proof kept by the house, made on a rented A5000 in 109 s

Declared progress (fingerprints linked to this problem)

Fingerprint my progress on this problem

• None yet.