lean_workbook_plus_65798Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)a2+ab+b2+b2+bc+c2=3(a+b2)2+(a−b2)2+3(b+c2)2+(b−c2)2\sqrt{a^2+ab+b^2}+\sqrt{b^2+bc+c^2}=\sqrt{3\left( \frac{a+b}{2}\right)^2+\left( \frac{a-b}{2}\right)^2}+\sqrt{3\left( \frac{b+c}{2}\right)^2+\left( \frac{b-c}{2}\right)^2}a2+ab+b2+b2+bc+c2=3(2a+b)2+(2a−b)2+3(2b+c)2+(2b−c)2Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_65798 (a b c : ℝ) : Real.sqrt (a ^ 2 + a * b + b ^ 2) + Real.sqrt (b ^ 2 + b * c + c ^ 2) = Real.sqrt (3 * (a + b) ^ 2 / 4 + (a - b) ^ 2 / 4) + Real.sqrt (3 * (b + c) ^ 2 / 4 + (b - c) ^ 2 / 4) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph