Prove2Me

lean_workbook_plus_51201

Disproved

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

Prove that:\n

1/2≤a24 a2+5 bc+b25 ac+4 b2+c25 ab+4 c21/2\leq \sqrt {{\frac {{a}^{2}}{4\,{a}^{2}+5\,bc}}}+\sqrt {{\frac {{b}^{2}}{5\,ac+4\,{b}^{2}}}}+\sqrt {{\frac {{c}^{2}}{5\,ab+4\,{c}^{2}}}}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_51201 : ∀ a b c : ℝ, (1 / 2 : ℝ) ≤ Real.sqrt (a^2 / (4 * a^2 + 5 * b * c)) + Real.sqrt (b^2 / (5 * a * c + 4 * b^2)) + Real.sqrt (c^2 / (5 * a * b + 4 * c^2))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph