lean_workbook_plus_8057Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)prove 2 ab+2 bc+2 ac≥(b+c−a)(a+b)(c+a)b+c+(a+c−b)(b+c)(a+b)c+a+(a+b−c)(c+a)(b+c)a+b2\,ab+2\,bc+2\,ac\geq {\frac { \left( b+c-a \right) \left( a+b \right) \left( c+a \right) }{b+c}}+{\frac { \left( a+c-b \right) \left( b+c \right) \left( a+b \right) }{c+a}}+{\frac { \left( a+b-c \right) \left( c+a \right) \left( b+c \right) }{a+b}}2ab+2bc+2ac≥b+c(b+c−a)(a+b)(c+a)+c+a(a+c−b)(b+c)(a+b)+a+b(a+b−c)(c+a)(b+c)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_8057 : ∀ a b c : ℝ, 2 * a * b + 2 * b * c + 2 * a * c ≥ (b + c - a) * (a + b) * (c + a) / (b + c) + (a + c - b) * (b + c) * (a + b) / (c + a) + (a + b - c) * (c + a) * (b + c) / (a + b) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph