lean_workbook_plus_81514

Proved

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

Let $a$ , $b$ , $c$ , $d$ , and $e$ be real numbers such that $ab + bc + cd + de + ea = 1$ and $ac + bd + ce + da + eb = -3$ . Prove that $a^2 + b^2 + c^2 + d^2 + e^2 \geq 4.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81514 (a b c d e : ℝ) (h1 : a * b + b * c + c * d + d * e + e * a = 1) (h2 : a * c + b * d + c * e + d * a + e * b = -3) : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 + e ^ 2 ≥ 4   :=  by sorry

Source

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

View graph