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

Versiunile criteriului · versiunea 2 (curentă)

Șablon: Teoremă verificată în Lean (enunțul e o declarație Lean; demonstrația o verifică nucleul) · Treapta de verificare: 0b — certificat ZK (demonstrații autonome)

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

Delimitări (ce NU acoperă criteriul): 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).

Provocarea (SHA-256): 686e2a073a93140c0270f14e89eb46df2f0669fdebd3353c4cbf95d66efa5150 · descarcă exportul provocării

Hash-ul pachetului: 8d068d1caa7ad48d4d5566672c74c38d257a9db8168c7efe1453e9877060e2e4 · #6

Semnături

• nicio semnătură încă

Certificate ZK legate de problemă

• #7 · succinct · 56 declarații verificate · ✓ corespunde provocării curente a problemei — Sealed comparator (v2): bound to this problem's challenge — proof kept by the house, made on a rented A5000 in 109 s

Progres declarat (amprente legate de problemă)

Amprentez progresul meu la această problemă

• Niciunul încă.