Prove2Me

lean_workbook_plus_74717

Disproved

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

2xy(z+x)(z+y)+2yz(x+y)(x+z)+3zx(y+z)(x+y)≥53  ⟺  x(y−2z)2+y(z−x)2+z(2x−y)2≥0\frac{2xy}{(z+x)(z+y)}+\frac{2yz}{(x+y)(x+z)}+\frac{3zx}{(y+z)(x+y)}\geq \frac{5}{3}\iff x(y-2z)^2+y(z-x)^2+z(2x-y)^2\geq 0
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_74717 : ∀ x y z : ℝ, (2*x*y/((z+x)*(z+y)) + 2*y*z/((x+y)*(x+z)) + 3*z*x/((y+z)*(x+y)) ≥ 5/3 ↔ x*(y-2*z)^2 + y*(z-x)^2 + z*(2*x-y)^2 ≥ 0)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph