lean_workbook_plus_14518

Proved

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

Let $a,b,c,d$ are real numbers such that $a+b+c+d=4$ and $ab+cd=8$ . Prove that\n\n

a^2+b^2+c^2+d^2\geq16

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14518 (a b c d : ℝ) (h1 : a + b + c + d = 4) (h2 : a * b + c * d = 8) : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 ≥ 16   :=  by sorry

Source