Submission cmph449m

by alice·5/22/2026, 5:06:51 PM

Accepted🌱 +5 Seeds awarded

Proof body (as submitted)

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

proof_body_hash: 66fca4a04c66cb582098f1bbcf00dea79d381942cde6b1337538efabfa54079f

Generated Lean file

What the judge actually compiles

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

import Leanforces.Challenges.C0001.Statement
import Mathlib

namespace Leanforces.Challenges.C0001.Submissions.Submission_cmph449ms0001u9imd7fk9i8l

-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
lemma h (n : Nat) : n + 0 = n := Nat.add_zero n
theorem answer (n : Nat) : n + 0 = n := h 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_cmph449ms0001u9imd7fk9i8l

file_hash (recomputed): 667287b9bbf6a225c033a16c1d3a278749cc53ef86dd346567a395b8aaa9fc51 ✓ matches stored hash

GitHub

Branchsubmission/cmph449ms0001u9imd7fk9i8l

Commit SHA2114e922d0255f904fffb895b17197d5d358c40f

Workflow runhttps://github.com/ryendo/leanforces-judge/actions/runs/26298617923

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, 5:08:57 PM	`legacy_solver_accept`	+5	solver	—