Prove2Me

lean_workbook_plus_5616

Proved

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

We have 1xyz≥9(xy+yz+xz)(x+y+z)\frac{1}{xyz} \geq \frac{9}{(xy + yz + xz)(x + y + z)}

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

View graph