lean_workbook_plus_47962

Proved

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

Let $x=\frac{bc}{a^2}$ , $y=\frac{ac}{b^2}$ and $z=\frac{ab}{c^2}$ , where $a$ , $b$ and $c$ are positives. \n Hence, $\left(\sum_{cyc}\frac{1}{\sqrt[3]{1+26x}}\right)^3\sum_{cyc}a^2(a^2+26bc)\geq(a+b+c)^4$ . \n Thus, it remains to prove that $(a+b+c)^4\geq\sum_{cyc}a^2(a^2+26bc)$ , which is obvious.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47962  (x y z a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : x = b * c / a^2)
  (h₂ : y = c * a / b^2)
  (h₃ : z = a * b / c^2) :
  (a + b + c)^4 ≥ a^2 * (a^2 + 26 * b * c) + b^2 * (b^2 + 26 * c * a) + c^2 * (c^2 + 26 * a * b)   :=  by sorry

Source

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

View graph