lean_workbook_plus_50587Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)a2a2+ab+b2+b2b2+bc+c2+c2c2+ca+a2+ab+bc+caa2+b2+c2≤2 \frac {a^2}{a^2 + ab + b^2} + \frac {b^2}{b^2 + bc + c^2} + \frac {c^2}{c^2 + ca + a^2} + \frac {ab + bc + ca}{a^2 + b^2 + c^2}\leq 2a2+ab+b2a2+b2+bc+c2b2+c2+ca+a2c2+a2+b2+c2ab+bc+ca≤2Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_50587 : ∀ a b c : ℝ, (a^2 / (a^2 + a * b + b^2) + b^2 / (b^2 + b * c + c^2) + c^2 / (c^2 + c * a + a^2) + (a * b + b * c + c * a) / (a^2 + b^2 + c^2) ≤ 2) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph