lean_workbook_plus_71714

Disproved

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

Prove that $(1 + x + y)^2 + (1 + y + z)^2 + (1 + z + x)^2 \leq 3(x + y + z)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71714 : ∀ x y z : ℝ, (1 + x + y) ^ 2 + (1 + y + z) ^ 2 + (1 + z + x) ^ 2 ≤ 3 * (x + y + z) ^ 2   :=  by sorry

Source