A product of quadratic and squared reciprocal sums is at least 27

Proved

WorkbookSource.base_38585

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that $\left(p^2+q^2+r^2 \right) \left(\frac{1}{p}+\frac{1}{q}+\frac{1}{r}\right) ^2 \ge 27$ given that $p, q,$ and $r$ are positive

Source: InternLM Lean-Workbook, record lean_workbook_38585 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_38585 (p q r : ℝ) (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) : (p^2 + q^2 + r^2) * (1 / p + 1 / q + 1 / r)^2 ≥ 27  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_38585; Apache-2.0

View graph