Prove2Me

lean_workbook_plus_67636

Proved

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

Prove that (xx+y)2+(yz+x)2+(zy+z)2≥13(xx+y+yz+x+zy+z)2(\frac{x}{x+y})^2 + (\frac{y}{z+x})^2 + (\frac{z}{y+z})^2 \geq \frac{1}{3}(\frac{x}{x+y}+\frac{y}{z+x}+\frac{z}{y+z})^2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67636 (x y z : ℝ) :
  (x / (x + y)) ^ 2 + (y / (z + x)) ^ 2 + (z / (y + z)) ^ 2 ≥
    1 / 3 * (x / (x + y) + y / (z + x) + z / (y + z)) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph