Submission cmpgw849

by alice·5/22/2026, 1:25:53 PM

Accepted🌱 +5 Seeds awarded

Proof body (as submitted)

exact Nat.add_zero n

proof_body_hash: a5d6a92f0ca08e1d373a3e7cf7c2c2479f3e06e655c9065e7489bce722f9c144

Generated Lean file

What the judge actually compiles

-- AUTO-GENERATED by ProofGarden Lean Judge. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgw849y0001xiowt1hzqd9p

import ProofGarden.Challenges.C0001.Statement
import Mathlib

namespace ProofGarden.Challenges.C0001.Submissions.Submission_cmpgw849y0001xiowt1hzqd9p

-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
exact Nat.add_zero n
-- └── USER SUBMISSION BODY END ────────────────────────────

/-- App-appended type check. Refuses to compile unless
    `answer` has type `∀ (n : Nat), n + 0 = n`. -/
def solution_target : ∀ (n : Nat), n + 0 = n := answer

#print axioms solution_target

end ProofGarden.Challenges.C0001.Submissions.Submission_cmpgw849y0001xiowt1hzqd9p

file_hash (recomputed): 13a016a25571d40f3ff689e0f8fc5fbd258269853ba2f2a6d02e1a1e21d134aa ✗ DOES NOT match stored hash

GitHub

Branchsubmission/cmpgw849y0001xiowt1hzqd9p

Commit SHAaf6339b86897e66f3aeebac8e79a942fabbad51f

Workflow runhttps://github.com/ryendo/proofgarden-judge/actions/runs/26287668151

PR #—