Prove2Me

A symmetric quartic inequality with lower-degree corrections

Proved
WorkbookSource.base_969

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

lean-workbooksource-checked

Let x,y,z>0x,y,z>0 ,prove

(x+y+z)2+6 xyz+(xy+xz+yz)2≥23 (xy+xz+yz)(2 x+3+2 y+2 z)+2 (x+y+z)xyz \left( x+y+z \right) ^{2}+6\,xyz+ \left( xy+xz+yz \right) ^{2}\geq \frac{2}{3}\, \left( xy+xz+yz \right) \left( 2\,x+3+2\,y+2\,z \right) +2\, \left( x+y+z \right) xyz

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_969 (x y z : ℝ) : (x + y + z) ^ 2 + 6 * x * y * z + (x * y + x * z + y * z) ^ 2 ≥ (2 / 3) * (x * y + x * z + y * z) * (2 * x + 3 + 2 * y + 2 * z) + 2 * (x + y + z) * x * y * z  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_969; Apache-2.0

View graph