A five-variable quadratic inequality over the reals

Proved

WorkbookSource.problem_40325

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

lean-workbooksource-checked

Prove that $2\sum_{i=1}^{5} r_i^2 \ge \sum_{1\le i < j \le 5} r_ir_j$ .

Source: InternLM Lean-Workbook, record lean_workbook_40325 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved. This version covers all real inputs; the related five-variable records plus_72847 and plus_10229 assume positivity.

Preamble

import Mathlib
open Real

Formal statement

theorem WorkbookSource.problem_40325 (r : ℕ → ℝ) : 2 * (r 1 ^ 2 + r 2 ^ 2 + r 3 ^ 2 + r 4 ^ 2 + r 5 ^ 2) ≥ r 1 * r 2 + r 1 * r 3 + r 1 * r 4 + r 1 * r 5 + r 2 * r 3 + r 2 * r 4 + r 2 * r 5 + r 3 * r 4 + r 3 * r 5 + r 4 * r 5  :=  by sorry

Source

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

View graph