lean_workbook_plus_31197Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)Prove that: \n 1a4+a2b2+b4+1b4+b2c2+c4+1c4+c2a2+a4≥9(a2+b2+c2)(ab+bc+ca) \frac {1}{{{a^4} + {a^2}{b^2} + {b^4}}} + \frac {1}{{{b^4} + {b^2}{c^2} + {c^4}}} + \frac {1}{{{c^4} + {c^2}{a^2} + {a^4}}} \ge \frac {9}{{\left( {{a^2} + {b^2} + {c^2}} \right)\left( {ab + bc + ca} \right)}}a4+a2b2+b41+b4+b2c2+c41+c4+c2a2+a41≥(a2+b2+c2)(ab+bc+ca)9Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_31197 : ∀ a b c : ℝ, (1 / (a ^ 4 + a ^ 2 * b ^ 2 + b ^ 4) + 1 / (b ^ 4 + b ^ 2 * c ^ 2 + c ^ 4) + 1 / (c ^ 4 + c ^ 2 * a ^ 2 + a ^ 4)) ≥ 9 / ((a ^ 2 + b ^ 2 + c ^ 2) * (a * b + b * c + c * a)) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph