A sixth-power inequality with a squared triple product

Proved

WorkbookSource.base_7774

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

lean-workbooksource-checked

The inequality is following to: $x^6+y^6+z^6+3x^2y^2z^2 \ge 2(x^3y^3+y^3z^3+z^3x^3)$

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

Preamble

import Mathlib
open Real Nat

Formal statement

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

Source