lean_workbook_plus_11176

Proved

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

From Cauchy we have \n\n ${3[(a}^{2}+b^{2}+c^{2})+(b^{2}+c^{2}+d^{2})+(c^{2}+d^{2}+a^{2})+(d^{2}+a^{2}+b^{2})]\geq(a+b+c)^{2}+(b+c+d)^{2}+(c+d+a)^{2}+(d+a+b)^{2}$ \n\n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11176 {a b c d : ℝ} :
  3 * ((a^2 + b^2 + c^2) + (b^2 + c^2 + d^2) + (c^2 + d^2 + a^2) + (d^2 + a^2 + b^2)) ≥
  (a + b + c)^2 + (b + c + d)^2 + (c + d + a)^2 + (d + a + b)^2   :=  by sorry

Source

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

View graph