Prove2Me

lean_workbook_plus_46273

Proved

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

Show that (x2+xy+y2)(z2+zt+t2)=((x+y/2)2+3y2/4)((t+z/2)2+3z2/4)≥((x+y/2)(t+z/2)+3yz/4)2(x^{2}+xy+y^{2}) (z^{2}+zt+t^{2}) = ((x+y/2)^{2}+3y^{2} / 4)((t+z/2)^{2} +3z^{2} / 4)\ge( (x+y/2)(t+z/2) + 3yz/4)^{2}

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

View graph