lean_workbook_plus_54686

Disproved

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

Best is:\n $\left( {x}^{5}+{y}^{5}+{z}^{5} \right) ^{6}\geq 243\,{x}^{6}{y}^{6}{z}^{6}\left( {x}^{12}+{y}^{12}+{z}^{12} \right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54686 :
  ∀ x y z : ℝ, (x^5 + y^5 + z^5)^6 ≥ 243 * x^6 * y^6 * z^6 * (x^12 + y^12 + z^12)   :=  by sorry

Source