Prove2Me

lean_workbook_plus_77561

Disproved

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

Prove this inequality \n (xy+z)2+(yx+z)2+(zx+y)2+6xyz(x+y)(y+z)(z+x)≥32{{\left( \frac{x}{y+z} \right)}^{2}}+{{\left( \frac{y}{x+z} \right)}^{2}}+{{\left( \frac{z}{x+y} \right)}^{2}}+\frac{6xyz}{\left( x+y \right)\left( y+z \right)\left( z+x \right)}\ge \frac{3}{2}

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

View graph