lean_workbook_plus_6289

Proved

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

We need to show that $26x^2+39y^2+52z^2\ge12(x+y+z)^2$ , or: $14x^2+27y^2+40z^2\ge24xy+24yz+24zx\Leftrightarrow2(3y-2x)^2+6(x-2z)^2+(3y-4z)^2\ge0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6289 (x y z : ℝ) :
  26 * x ^ 2 + 39 * y ^ 2 + 52 * z ^ 2 ≥ 12 * (x + y + z) ^ 2   :=  by sorry

Source