lean_workbook_plus_9810

Proved

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

Consider $S:=x^4+y^4+z^4-2y^2z^2-2z^2x^2-2x^2y^2=-(x+y+z)(y+z-x)(z+x-y)(x+y-z)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9810 : ∀ x y z : ℝ, x ^ 4 + y ^ 4 + z ^ 4 - 2 * y ^ 2 * z ^ 2 - 2 * z ^ 2 * x ^ 2 - 2 * x ^ 2 * y ^ 2 = -(x + y + z) * (y + z - x) * (z + x - y) * (x + y - z)   :=  by sorry

Source

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

View graph