Submission cmpgwa0q

by alice·5/22/2026, 1:27:22 PM

Accepted🌱 +5 Seeds awarded

Proof body (as submitted)

rfl

proof_body_hash: 5a633da644c1afc6f5222be040e6a19d687c01104c0263cce32773e07376dfa8

Generated Lean file

What the judge actually compiles

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

import ProofGarden.Challenges.C0001.Statement
import Mathlib

namespace ProofGarden.Challenges.C0001.Submissions.Submission_cmpgwa0qv0001x28ikntfrrjb

-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
rfl
-- └── 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_cmpgwa0qv0001x28ikntfrrjb

file_hash (recomputed): 83a91d3bb1b1229b2b9a531509e9e627be99e0a9eacdb23bb46068781bdca751 ✗ DOES NOT match stored hash

GitHub

Branchsubmission/cmpgwa0qv0001x28ikntfrrjb

Commit SHA5f202c669a0dcd9d6f6a31ec30ff4a7fa69967da

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

PR #—