C0002published🌱 10 Seeds (solver reward)
Ring expansion of (a + b)²
ShareProve that for every commutative ring and ,
Define answer : ∀ {R : Type _} [CommRing R] (a b : R), (a + b)^2 = a^2 + 2*a*b + b^2. Mathlib's ring tactic closes this in one line — but you're free to introduce helper lemmas. The app appends a def solution_target := answer type check after your body.
Theorem to prove
theorem answer {R : Type _} [CommRing R] (a b : R) : (a + b)^2 = a^2 + 2*a*b + b^2 := by
?You write Lean inside the wrapper namespace. Your body must define a top-level
answer with type ∀ {R : Type _} [CommRing R] (a b : R), (a + b)^2 = a^2 + 2*a*b + b^2. You can declare any def, theorem, lemma, instance, open, variable etc. — the static filter only blocks soundness-bypass tokens (sorry, axiom, native_decide, …) and wrapper-escape tokens (namespace, end, import, …).Sign in to submit a proof body.
Allowed proof-body format
Any sequence of Lean tactics is fine. The static filter rejects tokens that don't belong inside a tactic block — the full list:
importnamespacesectionenduniverseaxiomsorryadmitnative_decideopaqueconstantimplemented_byexternunsafemacrosyntaxelabrun_cmdinitializeset_optionattribute#eval#check#print#reduce#guardlocal attributesolution_targetRecent submissions