lean_workbook_plus_78793

Disproved

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

Prove that for all non-negative real numbers $a,b,c$ we always have\n $\frac{a(b+c-a)}{a^2+2bc}+\frac{b(c+a-b)}{b^2+2ca}+\frac{c(a+b-c)}{c^2+2ab} \ge 0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78793 :  ∀ a b c : ℝ, a ≥ 0 ∧ b ≥ 0 ∧ c ≥ 0 → a * (b + c - a) / (a ^ 2 + 2 * b * c) + b * (c + a - b) / (b ^ 2 + 2 * c * a) + c * (a + b - c) / (c ^ 2 + 2 * a * b) ≥ 0   :=  by sorry

Source

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

View graph