Prove2Me

lean_workbook_plus_61701

Disproved

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

Prove the corrected inequality:\n

ab+c+bc+a+ca+b+(a2−b2)(b2−c2)(c2−a2)(a2+b2)(b2+c2)(c2+a2)≥32\frac{a}{b+c}+\frac{b}{c+a}+\frac{c}{a+b} + \frac{\left(a^2-b^2\right)\left(b^2-c^2\right)\left(c^2-a^2\right)}{\left(a^2+b^2\right)\left(b^2+c^2\right)\left(c^2+a^2\right)} \ge \frac{3}{2}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61701 : ∀ a b c : ℝ, (a / (b + c) + b / (c + a) + c / (a + b) + (a^2 - b^2) * (b^2 - c^2) * (c^2 - a^2) / ((a^2 + b^2) * (b^2 + c^2) * (c^2 + a^2))) ≥ 3 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph