lean_workbook_plus_73665

Disproved

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

Now by AM-GM, $(6x+2y+2z)^5(5y+5z)^4\leq \frac{1}{9}\left( \frac{10}{3}(x+y+z)\right)^9$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73665 :  ∀ x y z : ℝ, (6 * x + 2 * y + 2 * z) ^ 5 * (5 * y + 5 * z) ^ 4 ≤  1 / 9 * (10 / 3 * (x + y + z)) ^ 9   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph