lean_workbook_plus_14152

Disproved

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

There is a nice proof for this inequality.\n\n $\dfrac{a^2}{a^2 +2bc} + \dfrac{b^2}{b^2+2ca} + \dfrac{c^2}{c^2+2ab} \geq \dfrac{(a+b+c)^2}{3(ab+bc+ca)}<=>$ \n\n $\dfrac{3a^2(ab+bc+ca)}{a^2 +2bc} + \dfrac{3b^2(ab+bc+ca)}{b^2+2ca} + \dfrac{3c^2(ab+bc+ca)}{c^2+2ab} \geq (a+b+c)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14152 : ∀ a b c : ℝ, (a^2 / (a^2 + 2 * b * c) + b^2 / (b^2 + 2 * c * a) + c^2 / (c^2 + 2 * a * b) ≥ (a + b + c) ^ 2 / (3 * (a * b + b * c + a * c)))   :=  by sorry

Source

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

View graph