Prove2Me

lean_workbook_plus_66470

Disproved

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

prove that: \n\n y2xz(y+x)2(xy+z2)+z2xy(y+z)2(zy+x2)+x2yz(z+x)2(xz+y2)≤38 \frac{y^{2}xz}{(y+x)^{2}(xy+z^{2})}+\frac{z^{2}xy}{(y+z)^{2}(zy+x^{2})}+\frac{x^{2}yz}{(z+x)^{2}(xz+y^{2})}\le\frac{3}{8} \n\n thanx.

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

View graph