lean_workbook_plus_48252

Disproved

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

Prove that for positive reals $a,b,c$ , \n $\frac {a^2 + ac}{2b + a + c} + \frac {b^2 + ba}{2c + a + b} + \frac {c^2 + cb}{2a + b + c} \ge 2(a + b + c)$ \nwhen does the equality hold?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48252 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (a^2 + a*c)/(2*b + a + c) + (b^2 + b*a)/(2*c + a + b) + (c^2 + c*b)/(2*a + b + c) ≥ 2*(a + b + c)   :=  by sorry

Source

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

View graph