lean_workbook_plus_43557

Proved

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

and we need to prove that $3(a+b+c+d)^2 \ge 8(ab+ac+ad+bc+bd+cd)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source