Prove2Me

lean_workbook_plus_54836

Disproved

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

Prove that\n\n∑(a−b)2(b−c)2(c−a)2(a+b)(a+c)(a2+bc)≥0. \sum \frac {(a - b)^2(b - c)^2(c - a)^2}{(a + b)(a + c)(a^2 + bc) }\ge 0.

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

View graph