Prove2Me

lean_workbook_plus_12721

Proved

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

Prove that (x−y)4+(y−z)4+(z−x)4=2(x2+y2+z2−xy−yz−zx)2(x-y)^4+(y-z)^4+(z-x)^4=2(x^2+y^2+z^2-xy-yz-zx)^2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12721 (x y z : ℝ) :
  (x - y) ^ 4 + (y - z) ^ 4 + (z - x) ^ 4 =
    2 * (x ^ 2 + y ^ 2 + z ^ 2 - x * y - y * z - z * x) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph