lean_workbook_plus_50840

Disproved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $\left( {a}^{2}+bc \right) ^{-1}+ \left( {b}^{2}+ac \right) ^{-1}+ \left( {c}^{2}+ab \right) ^{-1}\geq 3\, \left( ab+ac+bc \right) ^{-1}+{\frac {243}{2}}\,{\frac {{a}^{2}{b}^{2}{c}^{2}}{ \left( a+b+c \right) ^{2} \left( ab+ac+bc \right) ^{3}}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50840 : ∀ a b c : ℝ, (a^2 + b * c)^(-1:ℤ) + (b^2 + a * c)^(-1:ℤ) + (c^2 + a * b)^(-1:ℤ) ≥ 3 * (a * b + a * c + b * c)^(-1:ℤ) + (243 / 2) * (a^2 * b^2 * c^2) / ((a + b + c)^2 * (a * b + a * c + b * c)^3)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph