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 Leanforces. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgwa0qv0001x28ikntfrrjb

import Leanforces.Challenges.C0001.Statement
import Mathlib

namespace Leanforces.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 Leanforces.Challenges.C0001.Submissions.Submission_cmpgwa0qv0001x28ikntfrrjb

file_hash (recomputed): 120e4a26c1bf202564cd0bbb718a402cb4d841d6fc88ed3be64af1c7554246a0 ✗ DOES NOT match stored hash

GitHub

Branchsubmission/cmpgwa0qv0001x28ikntfrrjb

Commit SHA5f202c669a0dcd9d6f6a31ec30ff4a7fa69967da

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

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, 1:28:06 PM	`legacy_solver_accept`	+5	solver	—