lean_workbook_plus_13322

Proved

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

If $x$ , $y$ and $z$ are positive real numbers, prove \n\n

\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_13322  (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) :
  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