lean_workbook_plus_57742

Disproved

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

For all $x,y,z \geqslant 0$ , show that \n $\left( x^2y+y^2z+z^2x\right) \cdot \left(\frac{1}{(x-y)^2}+\frac{1}{(y-z)^2} +\frac{1}{(z-x)^2}\right) \geqslant \frac45 \left(x+y+z\right)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57742 : ∀ x y z : ℝ, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 → (x^2*y + y^2*z + z^2*x) * (1/(x-y)^2 + 1/(y-z)^2 + 1/(z-x)^2) ≥ 4/5 * (x + y + z)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph