lean_workbook_plus_79819

Proved

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

Prove that $\frac{1}{p(p+1)}+\frac{1}{q(q+1)}{\ge}\frac{1}{3}$ given $p,q>0$ and $\frac{1}{p}+\frac{1}{q}=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79819 (p q : ℝ) (hp : 0 < p) (hq : 0 < q) (h : 1 / p + 1 / q = 1) : 1 / (p * (p + 1)) + 1 / (q * (q + 1)) ≥ 1 / 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph