lean_workbook_plus_63175

Disproved

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

Prove that $2(\sqrt{x(y^{29}+z^{2007})}+\sqrt{y^{29}(x+z^{2007})}+\sqrt{z^{2007}(x+y^{29})})\leq3(x+y^{29}+z^{2007})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63175 : ∀ x y z : ℝ, 2 * (Real.sqrt (x * (y^29 + z^2007)) + Real.sqrt (y^29 * (x + z^2007)) + Real.sqrt (z^2007 * (x + y^29))) ≤ 3 * (x + y^29 + z^2007)   :=  by sorry

Source

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

View graph