lean_workbook_plus_72135

Proved

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

We'll use Ravi's substitution: \n\n

a=x+y,b=y+z,c=z+x(x,y,z > 0)

\frac{a}{b+c} + \frac{b}{c+a} + \frac{c}{a+b}< 2 \Leftrightarrow \sum_{cyc}\frac{x+y}{x+y+2z} < 2 \Leftrightarrow \sum_{cyc}1-\frac{x+y}{x+y+2z}>1\Leftrightarrow\sum_{cyc}\frac{z}{x+y+2z}>\frac{1}{2}

\Leftrightarrow\sum_{cyc}\frac{z^2}{xz+yz+2z^2}>\frac{1}{2}

\sum_{cyc}\frac{z^2}{xz+yz+2z^2}\ge\frac{(x+y+z)^2}{2x^2+2y^2+2z^2+2xy+2xz+2yz}(C-S)

$\Rightarrow$ It suffices to prove that $2(x+y+z)^2>2x^2+2y^2+2z^2+2xy+2xz+2yz\Leftrightarrow 2xy+2yz+2zx>0$ ,which is obvious.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_72135  (x y z : ℝ)
  (h₀ : 0 < x ∧ 0 < y ∧ 0 < z) :
  (x + y) / (x + y + 2 * z) + (y + z) / (y + z + 2 * x) + (z + x) / (z + x + 2 * y) < 2   :=  by sorry

Source

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

View graph