Prove2Me

A reciprocal sum bounds weighted quadratic reciprocals

Proved
WorkbookSource.base_27509

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

lean-workbooksource-checked

If a,b,c>0 a,b,c>0 prove that :

1a+1b+1c≥4a2a2+b2+c2+4b2b2+c2+a2+4c2c2+a2+b2 \frac{1}{a}+\frac{1}{b}+\frac{1}{c}\ge \frac{4a}{2a^2+b^2+c^2}+\frac{4b}{2b^2+c^2+a^2}+\frac{4c}{2c^2+a^2+b^2}

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_27509 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (1 / a + 1 / b + 1 / c) ≥ (4 * a / (2 * a ^ 2 + b ^ 2 + c ^ 2) + 4 * b / (2 * b ^ 2 + c ^ 2 + a ^ 2) + 4 * c / (2 * c ^ 2 + a ^ 2 + b ^ 2))  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_27509; Apache-2.0

View graph