GitHub failed
Proof body (as submitted)
theorem answer {R : Type _} [CommRing R] (a b : R) : (a + b)^2 = a^2 + 2*a*b + b^2 := by ringproof_body_hash:
91fd2504f0005b01e2ab080dae2cb1bb405056c2470cb1c67d38949d1e4d5d1dGenerated Lean file
What the judge actually compiles
-- AUTO-GENERATED by Leanforces. Do not edit by hand.
-- Challenge: C0002
-- Submission: cmpgy3b8x000111l6zxdyfoh2
import Mathlib
namespace Leanforces.Challenges.C0002.Submissions.Submission_cmpgy3b8x000111l6zxdyfoh2
-- ┌── 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_cmpgy3b8x000111l6zxdyfoh2
file_hash (recomputed):
dbbdf2058c868455c5c2f9a4f95ff47f7a94ce39b0e13664742d29b5c6cb98ab ✗ DOES NOT match stored hashGitHub
Branchsubmission/cmpgy3b8x000111l6zxdyfoh2
Commit SHAb4728b66bb5b054ff4935f58953b1e2c400431c2
PR #—