Prove2Me

A squared cubic sum bounds a triangle-factor quadratic sum

Proved
WorkbookSource.plus_10270

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

lean-workbooksource-checked

If x,y,z≥0x,y,z \ge 0 Prove that : 27(∑x3)2≥(∑x)4∑(y+z−x)227(\sum{x^3})^2 \ge (\sum{x})^4\sum{(y+z-x)^2}

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

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

View graph