Prove2Me

A squared cubic sum bounds a cyclic quartic-square sum

Proved
WorkbookSource.base_29873

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

lean-workbooksource-checked

Let a=xy,a=\frac{x}{y}, b=yz,b=\frac{y}{z}, where xx , yy and zz are positives. Thus, c=zxc=\frac{z}{x} and we need to prove that:

(x3+y3+z3)2≥3(x4z2+y4x2+z4y2)(x^3+y^3+z^3)^2\geq3(x^4z^2+y^4x^2+z^4y^2)

or

∑cycy3(x−y)2(2x+y)≥0.\sum_{cyc}y^3(x-y)^2(2x+y)\geq0.

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

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

View graph