lean_workbook_plus_67435

Proved

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

Let $a=\frac{y}{x+y},b=\frac{z}{y+z},c=\frac{x}{z+x}$ . Rewrite the original inequality as $\sum b(1-b)+2\sum a(1-c)\leq \frac{9}{4}$ . Simplify and prove.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67435 (x y z : ℝ) :
  (y / (x + y) * (1 - y / (x + y)) + z / (y + z) * (1 - z / (y + z)) + x / (z + x) * (1 - x / (z + x))) ≤ 9 / 4   :=  by sorry

Source

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

View graph