Prove2Me

lean_workbook_plus_12719

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Euhm... x2+x=y2+y ⟺ (x2−y2)+(x−y)=(x−y)(x+y+1)=0x^{2}+x=y^{2}+y\ \Longleftrightarrow\ \left(x^{2}-y^{2}\right)+\left(x-y\right) = (x-y)(x+y+1) = 0 ...

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12719 : ∀ x y : ℤ, x^2 + x = y^2 + y ↔ (x - y) * (x + y + 1) = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph