lean_workbook_plus_6272

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Hence, it remains to prove that $(x^3+y^3+z^3)^8\geq243\left(x^4y^4+x^4z^4+y^4z^4\right)^3,$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6272 : ∀ x y z : ℝ, (x ^ 3 + y ^ 3 + z ^ 3) ^ 8 ≥ 243 * (x ^ 4 * y ^ 4 + x ^ 4 * z ^ 4 + y ^ 4 * z ^ 4) ^ 3   :=  by sorry

Source