lean_workbook_plus_77590Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)2ab+c2≥2abc(1a+b+1b+c+1c+a)⇔a2(b+c)(c−b)2+b2(c+a)(c−a)2+(a+b)(ab−c2)2≥02ab+c^2 \ge 2abc(\frac{1}{a+b}+\frac{1}{b+c}+\frac{1}{c+a}) \Leftrightarrow {{a}^{2}}\left( b+c \right){{\left( c-b \right)}^{2}}+{{b}^{2}}\left( c+a \right){{\left( c-a \right)}^{2}}+\left( a+b \right){{\left( ab-{{c}^{2}} \right)}^{2}}\ge 02ab+c2≥2abc(a+b1+b+c1+c+a1)⇔a2(b+c)(c−b)2+b2(c+a)(c−a)2+(a+b)(ab−c2)2≥0Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_77590 : ∀ a b c : ℝ, 2 * a * b + c ^ 2 ≥ 2 * a * b * c * (1 / (a + b) + 1 / (b + c) + 1 / (c + a)) ↔ a ^ 2 * (b + c) * (c - b) ^ 2 + b ^ 2 * (c + a) * (c - a) ^ 2 + (a + b) * (a * b - c ^ 2) ^ 2 ≥ 0 := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph