A sixth-degree bound under a weighted zero sum

Proved

WorkbookSource.base_41374

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

lean-workbooksource-checked

Let $x,y,z$ are real numbers such that $x+3y+z=0$ . Prove that

\left(x^2+y^2+z^2\right)^3\geq \frac{38}{27}\left(x^3+y^3+z^3\right)^2

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_41374 (x y z : ℝ) (h : x + 3 * y + z = 0) :
  (x^2 + y^2 + z^2)^3 ≥ (38/27) * (x^3 + y^3 + z^3)^2  :=  by sorry

Source