A quintic inequality under weighted triangle constraints

Proved

WorkbookSource.plus_61283

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

prove that

$\left( {x}^{2}+{y}^{2}+{z}^{2} \right) xyz-1/9\, \left( x+y+z \right) \left( xy+zx+yz \right) ^{2}\geq 0,[7/5\,z\leq x+y,7/5\,x\leq y+z,7/5\,y\leq z+x]$

Source: InternLM Lean-Workbook, record lean_workbook_plus_61283 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_61283 {x y z : ℝ} (hx : 7 / 5 * z ≤ x + y) (hy : 7 / 5 * x ≤ y + z) (hz : 7 / 5 * y ≤ z + x) : (x ^ 2 + y ^ 2 + z ^ 2) * x * y * z - 1 / 9 * (x + y + z) * (x * y + y * z + z * x) ^ 2 ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_61283; Apache-2.0

View graph