Prove2Me

lean_workbook_plus_79950

Proved

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

Note that 12((x3+14x2−2x)−(y3+14y2−2y))=(x−y)(3(2x+y+14)2+(3y+14)2−808)12((x^3+14x^2-2x)-(y^3+14y^2-2y))=(x-y)(3(2x+y+14)^2+(3y+14)^2-808)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79950 : ∀ x y : ℝ, 12 * (x^3 + 14 * x^2 - 2 * x - (y^3 + 14 * y^2 - 2 * y)) = (x - y) * (3 * (2 * x + y + 14)^2 + (3 * y + 14)^2 - 808)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph