Prove2Me

lean_workbook_plus_13420

Proved

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

Prove that 2∑(x+y)2z≤3(x+y)(y+z)(z+x)2 \sum (x+y)^2z \leq 3 (x+y)(y+z)(z+x) for positive reals x, y, z.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13420 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : 2 * (x + y) ^ 2 * z + 2 * (y + z) ^ 2 * x + 2 * (z + x) ^ 2 * y ≤ 3 * (x + y) * (y + z) * (z + x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph