lean_workbook_plus_27328

Proved

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

Let $a,b,c,d$ be real numbers, such that $a^2\le 1, a^2 + b^2\le 5, a^2 + b^2 + c^2\le 14, a^2 + b^2 + c^2 + d^2\le 30$ . Prove that $a + b + c + d\le 10$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27328 (a b c d : ℝ) (ha : a ^ 2 ≤ 1) (hb : a ^ 2 + b ^ 2 ≤ 5) (hc : a ^ 2 + b ^ 2 + c ^ 2 ≤ 14) (hd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 ≤ 30) : a + b + c + d ≤ 10   :=  by sorry

Source

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

View graph