Prove2Me

lean_workbook_plus_72909

Disproved

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

Prove that:\n

1/2+1/2 ab+ca+bca2+b2+c2≤a24 a2+5 bc+b25 ca+4 b2+c25 ab+4 c21/2+1/2\,\sqrt {{\frac {ab+ca+bc}{{a}^{2}+{b}^{2}+{c}^{2}}}}\leq \sqrt {{\frac {{a}^{2}}{4\,{a}^{2}+5\,bc}}}+\sqrt {{\frac {{b}^{2}}{5\,ca+4\,{b}^{2}}}}+\sqrt {{\frac {{c}^{2}}{5\,ab+4\,{c}^{2}}}}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72909 : ∀ a b c : ℝ, 1 / 2 + 1 / 2 * Real.sqrt ((a * b + b * c + c * a) / (a ^ 2 + b ^ 2 + c ^ 2)) ≤ Real.sqrt (a ^ 2 / (4 * a ^ 2 + 5 * b * c)) + Real.sqrt (b ^ 2 / (5 * c * a + 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