lean_workbook_plus_2328

Proved

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

If $b+c+d+e=0$ , we're done. Otherwise, as the required inequality is homogeneous, we may assume $b+c+d+e = 1$ . Then $b^2+c^2+d^2+e^2 \ge 1/4$ by Cauchy-Schwarz, and it is enough to prove $a^2-a+1/4 = (a-1/2)^2 \ge 0$ , which is true.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2328  (b c d e a : ℝ)
  (h₀ : b + c + d + e = 0)
  (h₁ : a + b + c + d + e = 1) :
  a^2 + b^2 + c^2 + d^2 + e^2 ≥ 1 / 4   :=  by sorry

Source

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

View graph