A cyclic cubic lower bound under a quartic norm constraint

Proved

WorkbookSource.base_3816

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

lean-workbooksource-checked

Let $x;y;z$ be real number such that $x^4+y^4+z^4=3$ Prove: $x^2(x+y)+y^2(y+z)+z^2(z+x) \geq -6$

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

Preamble

import Mathlib
open Real Nat

Formal statement

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

Source

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

View graph