Prove2Me

lean_workbook_plus_41654

Proved

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

If xx , yy and zz are positive real numbers, prove \n\n

1x+1y+1z≥4(x+y+z)2−3(xy+yz+zx)(x+y+z)(xy+yz+zx)\dfrac{1}{x} + \dfrac {1}{y} + \dfrac {1}{z} \geq \dfrac{4(x+y+z)^2-3(xy+yz+zx)}{(x+y+z)(xy+yz+zx)}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_41654 (x y z : ℝ) : x > 0 ∧ y > 0 ∧ z > 0 → 1/x + 1/y + 1/z ≥ (4 * (x + y + z) ^ 2 - 3 * (x*y + y*z + z*x)) / (x + y + z) / (x*y + y*z + z*x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph