An asymmetric sixth-power inequality with cubic products

Proved

WorkbookSource.plus_74167

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

lean-workbooksource-checked

Let $a=x^2,b=y^2,c=z^2$ .The given inequality is equivalent to $4z^6+x^6+y^6+3x^2y^2(x^2+y^2)\ge 4(x^3y^3+y^3z^3+z^3x^3)$ .

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_74167 (x y z : ℝ) : 4 * z ^ 6 + x ^ 6 + y ^ 6 + 3 * x ^ 2 * y ^ 2 * (x ^ 2 + y ^ 2) ≥ 4 * (x ^ 3 * y ^ 3 + y ^ 3 * z ^ 3 + z ^ 3 * x ^ 3)   :=  by sorry

Source

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

View graph