Prove2Me

lean_workbook_plus_16767

Disproved

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

prove that \n xt+1(y−z)2+yt+1(z−x)2+zt+1(x−y)2≥12 (xt+yt+zt)(x+y−2 z)(y+z−2 x)(z+x−2 y){x}^{t+1} \left( y-z \right) ^{2}+{y}^{t+1} \left( z-x \right) ^{2}+{z}^{t+1} \left( x-y \right) ^{2}\geq \frac{1}{2}\, \left( {x}^{t}+{y}^{t}+{z}^{t} \right) \left( x+y-2\,z \right) \left( y+z-2\,x \right) \left( z+x-2\,y \right)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16767 :  ∀ x y z : ℝ, ∀ t : ℕ, x^(t + 1) * (y - z)^2 + y^(t + 1) * (z - x)^2 + z^(t + 1) * (x - y)^2 ≥ 1 / 2 * (x^t + y^t + z^t) * (x + y - 2 * z) * (y + z - 2 * x) * (z + x - 2 * y)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph