lean_workbook_plus_67347

Disproved

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

Yes, it's easy. After using Cauchy-Schwarz it remains to prove that $8(xy+xz+yz)(x+y+z)\leq9(x+y)(x+z)(y+z)$ , which is obvious.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67347 : ∀ x y z : ℝ, 8 * (x * y + x * z + y * z) * (x + y + z) ≤ 9 * (x + y) * (x + z) * (y + z)   :=  by sorry

Source