Prove2Me

lean_workbook_plus_55444

Proved

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

Show that ∑x(1−y2−z2+y2z2)=∑x+xyz−∑xy(x+y)=4xyz\sum {x\left( {1 - y^2 - z^2 + y^2 z^2 } \right)} = \sum x + xyz - \sum {xy\left( {x + y} \right)} = 4xyz given x,y,z≥0x,y,z\geq 0 and xy+xz+yz=1xy + xz + yz = 1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55444 {x y z : ℝ} (hx : x ≥ 0) (hy : y ≥ 0) (hz : z ≥ 0) (h : x * y + x * z + y * z = 1) : x * (1 - y ^ 2 - z ^ 2 + y ^ 2 * z ^ 2) + y * (1 - z ^ 2 - x ^ 2 + z ^ 2 * x ^ 2) + z * (1 - x ^ 2 - y ^ 2 + x ^ 2 * y ^ 2) = 4 * x * y * z   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph