Prove2Me

lean_workbook_plus_23117

Disproved

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

For x,y,z>0x,y,z>0 real numbers, prove that:\nx(y+z)+y(x+z)+z(x+y)+8xyzx+y+z≥5(x+y)(y+z)(z+x)x+y+z  ;x(y+z) + y(x+z) + z(x+y) + \frac{8xyz}{x+y+z} \ge \frac{5(x+y)(y+z)(z+x)}{x+y+z} \ \ ;\n\nTry z→0+z\rightarrow0^+ .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23117 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : x * (y + z) + y * (x + z) + z * (x + y) + 8 * x * y * z / (x + y + z) ≥ 5 * (x + y) * (y + z) * (z + x) / (x + y + z)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph