lean_workbook_plus_55363

Proved

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

Prove or disprove: For all real numbers $a_1,a_2,a_3,b,c,d$ : $a_1^2+a_2^2+a_3^2+b^2+c^2+d^2\ge2(a_1a_3+a_1a_2-a_2a_3+bc+bd-cd)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55363 : ∀ a₁ a₂ a₃ b c d : ℝ, a₁^2 + a₂^2 + a₃^2 + b^2 + c^2 + d^2 ≥ 2 * (a₁ * a₃ + a₁ * a₂ - a₂ * a₃ + b * c + b * d - c * d)   :=  by sorry

Source

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

View graph