Prove2Me

lean_workbook_plus_82601

Proved

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

We have: 3≥1x+1y+1z⇒3(1x+1y+1z)≥(1x+1y+1z)23\geq \frac{1}{x}+\frac{1}{y}+\frac{1}{z}\Rightarrow 3(\frac{1}{x}+\frac{1}{y}+\frac{1}{z})\geq (\frac{1}{x}+\frac{1}{y}+\frac{1}{z})^{2}

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

View graph