Prove2Me

lean_workbook_plus_63571

Disproved

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

The following inequality is also true:\n ab+c+bc+a+ca+b≥72−16abc(a+b+c)3+5abc\frac{a}{b+c}+\frac{b}{c+a}+\frac{c}{a+b}\ge\frac{7}{2}-\frac{16abc}{(a+b+c)^3+5abc}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_63571 : ∀ a b c : ℝ, (a / (b + c) + b / (c + a) + c / (a + b) ≥ 7 / 2 - 16 * a * b * c / ((a + b + c) ^ 3 + 5 * a * b * c))   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph