lean_workbook_plus_28691

Proved

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

Now: $a+b+c=7-d,a^{2}+b^{2}+c^{2}=13-d^{2}$ and it is well-known (e.g. by sums of squares) that $3\left(a^{2}+b^{2}+c^{2}\right)\geq\left(a+b+c\right)^{2}$ for all $a,b,c\in\mathbb{R}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28691  (a b c d : ℝ)
  (h₀ : a + b + c = 7 - d)
  (h₁ : a^2 + b^2 + c^2 = 13 - d^2) :
  3 * (a^2 + b^2 + c^2) ≥ (a + b + c)^2   :=  by sorry

Source

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

View graph