lean_workbook_plus_29237

Proved

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

Given $a-b=x, b-c=y, c-a=z$ , prove that $a^3x^2z^2+b^3x^2y^2+c^3y^2z^2-(a+b+c)x^2y^2z^2$ is equivalent to $(axz+bxy+cyz)\left(a^2xz+b^2xy+c^2yz\right)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29237 (a b c x y z : ℝ) (hx : x = a - b) (hy : y = b - c) (hz : z = c - a) : a^3 * x^2 * z^2 + b^3 * x^2 * y^2 + c^3 * y^2 * z^2 - (a + b + c) * x^2 * y^2 * z^2 = (a * x * z + b * x * y + c * y * z) * (a^2 * x * z + b^2 * x * y + c^2 * y * z)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph