lean_workbook_plus_72967Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)ab2+c2+bc2+a2+ca2+b2≥45(1a+b+1b+c+1c+a)+81abc10(a+b+c)2(ab+bc+ca)\dfrac{a}{b^2+c^2}+\dfrac{b}{c^2+a^2}+\dfrac{c}{a^2+b^2}\geq \dfrac{4}{5}\left(\dfrac{1}{a+b}+\dfrac{1}{b+c}+\dfrac{1}{c+a}\right)+\dfrac{81abc}{10(a+b+c)^2(ab+bc+ca)}b2+c2a+c2+a2b+a2+b2c≥54(a+b1+b+c1+c+a1)+10(a+b+c)2(ab+bc+ca)81abc is also true.Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_72967 : ∀ a b c : ℝ, (a / (b ^ 2 + c ^ 2) + b / (c ^ 2 + a ^ 2) + c / (a ^ 2 + b ^ 2) ≥ 4 / 5 * (1 / (a + b) + 1 / (b + c) + 1 / (c + a)) + 81 * a * b * c / (10 * (a + b + c) ^ 2 * (a * b + b * c + c * a))) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph