Prove2Me

lean_workbook_plus_54144

Disproved

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

Let x,y,z>0 x, y, z > 0 . Prove that the following inequality holds: x2+y2+z2xy+yz+zx≥1+(x+yz+z+xy+y+zx)−4(xy+z+yz+x+zx+y). \frac {x^2 + y^2 + z^2}{xy + yz + zx}\geq 1 + \left(\frac {x + y}{z} + \frac {z + x}{y} + \frac {y + z}{x}\right) - 4\left(\frac {x}{y + z} + \frac {y}{z + x} + \frac {z}{x + y}\right).

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

View graph