Prove2Me

A symmetric sixth-degree inequality with a difference correction

Proved
WorkbookSource.base_56355

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

lean-workbooksource-checked

Prove that (x3+y3+z3)2+3(xyz)2≥4(y3z3+z3x3+x3y3)+45[(x−y)2(y−z)2(z−x)2](x^3+y^3+z^3)^2+3( xyz )^2\geq 4( y^3z^3+z^3x^3+x^3y^3)+ \frac45 [ (x-y)^2(y-z)^2(z-x)^2 ] for x,y,z∈Rx,y,z \in R.

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

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

View graph