lean_workbook_plus_16301

Proved

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

For $n = 4$ , prove that the inequality $(a_{1} + a_{2} + a_{3} + a_{4})^{2} - 4(a_{1}a_{2} + a_{2}a_{3} + a_{3}a_{4} + a_{4}a_{1}) \geqslant 0$ holds.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16301 (a : ℕ → ℝ) : (a 1 + a 2 + a 3 + a 4) ^ 2 - 4 * (a 1 * a 2 + a 2 * a 3 + a 3 * a 4 + a 4 * a 1) ≥ 0   :=  by sorry

Source

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

View graph