Submission cmpgy8ng

by alice·5/22/2026, 2:22:17 PM

Accepted🌱 +10 Seeds awarded

Proof body (as submitted)

theorem answer {R : Type _} [CommRing R] (a b : R) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring

proof_body_hash: 91fd2504f0005b01e2ab080dae2cb1bb405056c2470cb1c67d38949d1e4d5d1d

Generated Lean file

What the judge actually compiles

-- AUTO-GENERATED by Leanforces. Do not edit by hand.
-- Challenge: C0002
-- Submission: cmpgy8ngz0001ufk8gc8oy8bi

import Mathlib

namespace Leanforces.Challenges.C0002.Submissions.Submission_cmpgy8ngz0001ufk8gc8oy8bi

-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
theorem answer {R : Type _} [CommRing R] (a b : R) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ring
-- └── USER SUBMISSION BODY END ────────────────────────────

/-- App-appended type check. Refuses to compile unless
    `answer` has type `∀ {R : Type _} [CommRing R] (a b : R), (a + b)^2 = a^2 + 2*a*b + b^2`. -/
def solution_target : ∀ {R : Type _} [CommRing R] (a b : R), (a + b)^2 = a^2 + 2*a*b + b^2 := answer

#print axioms solution_target

end Leanforces.Challenges.C0002.Submissions.Submission_cmpgy8ngz0001ufk8gc8oy8bi

file_hash (recomputed): 3e3874f3e6b13b2ff9e4915a3f878e8c28a1c3621e83bb1d78841ce84d0ad639 ✗ DOES NOT match stored hash

GitHub

Branchsubmission/cmpgy8ngz0001ufk8gc8oy8bi

Commit SHAb95ac1d9568cff3fbd882719a82115c7229a52ab

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

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:21 PM	`legacy_solver_accept`	+10	solver	—