lean_workbook_plus_4687

Disproved

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

prove that \n $\boxed{\frac{a}{a^{2}+2bc}+\frac{b}{b^{2}+2ca}+\frac{c}{c^{2}+2ab}\leq\frac{a+b+c}{ab+bc+ca}}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4687 : ∀ a b c : ℝ, (a / (a ^ 2 + 2 * b * c) + b / (b ^ 2 + 2 * c * a) + c / (c ^ 2 + 2 * a * b) ≤ (a + b + c) / (a * b + b * c + a * c))   :=  by sorry

Source

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

View graph