Prove2Me

lean_workbook_plus_21283

Disproved

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

x2+yzy2+z2+y2+xzx2+z2+z2+xyy2+x2≥5/2+4 xyz(y+z)(z+x)(x+y){\frac {{x}^{2}+yz}{{y}^{2}+{z}^{2}}}+{\frac {{y}^{2}+xz}{{x}^{2}+{z}^{2}}}+{\frac {{z}^{2}+xy}{{y}^{2}+{x}^{2}}}\geq 5/2+4\,{\frac {xyz}{ \left( y+z \right) \left( z+x \right) \left( x+y \right) }}

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

View graph