lean_workbook_plus_10801

Proved

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

Prove that if $a, b, c$ and $d$ are real numbers, then \n

a + b+ c + d - a^2 -b^2 -c^2 - d^2 \leq1 .

(21st Transylvanian Hungarian Mathematical Competition, 2011)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10801 (a b c d : ℝ) : a + b + c + d - a ^ 2 - b ^ 2 - c ^ 2 - d ^ 2 ≤ 1   :=  by sorry

Source