Prove2Me

lean_workbook_plus_23128

Disproved

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

Prove that \n (y+z−x)2(y+z)2+x2+(z+x−y)2(z+x)2+y2+(x+y−z)2(x+y)2+z2⩽3\frac{(y+z-x)^2}{(y+z)^2+x^2}+\frac{(z+x-y)^2}{(z+x)^2+y^2}+\frac{(x+y-z)^2}{(x+y)^2+z^2} \leqslant 3

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

View graph