lean_workbook_plus_18867

Proved

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

substitution $a=x+y,b=y+z,c=z+x$ ( $x,y,z>0$ )\n\nThe following inequality is equivalent to\n\n $2(x^2+5xy+y^2+5zx+5yz+z^2)(x^2-xy+y^2-zx-yz+z^2)\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18867 {x y z : ℝ} (hx : x > 0) (hy : y > 0) (hz : z > 0) : 2 * (x^2 + 5 * x * y + y^2 + 5 * z * x + 5 * z * y + z^2) * (x^2 - x * y + y^2 - z * x - z * y + z^2) ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph