Submission cmpgy89f

by alice·5/22/2026, 2:21:59 PM

Accepted🌱 +5 Seeds awarded

Proof body (as submitted)

lemma helper (n : Nat) : n + 0 = n := Nat.add_zero n
theorem answer (n : Nat) : n + 0 = n := helper n

proof_body_hash: 8909d528b93d0b1a39e75c3e6558558920a60747b01020c8ea2070a2b54f0a5a

Generated Lean file

What the judge actually compiles

-- AUTO-GENERATED by Leanforces. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgy89ff00019ge4qa0lxyh2

import Leanforces.Challenges.C0001.Statement
import Mathlib

namespace Leanforces.Challenges.C0001.Submissions.Submission_cmpgy89ff00019ge4qa0lxyh2

-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
lemma helper (n : Nat) : n + 0 = n := Nat.add_zero n
theorem answer (n : Nat) : n + 0 = n := helper 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 Leanforces.Challenges.C0001.Submissions.Submission_cmpgy89ff00019ge4qa0lxyh2

file_hash (recomputed): 585d68930175dc6a7506bd8d1bf3e0aff66d12e170b1ec846ab3996a0264c31b ✗ DOES NOT match stored hash

GitHub

Branchsubmission/cmpgy89ff00019ge4qa0lxyh2

Commit SHA1d6e421fbe965ed063d52760a1fccc71764d350f

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

PR #—

Seeds ledger entries for this submission

Append-only. Each row is one balance change in one user's account. There is no row that moves Seeds between two users — for two-sided events you'll see two rows sharing the “related” column.

When	Category	Δ	Bucket	Related
5/22/2026, 2:24:03 PM	`legacy_solver_accept`	+5	solver	—