lean_workbook_plus_5548

Disproved

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

Prove that $(a+b)^{2}(c^{2}+d^{2})\geqslant (ac+bd)^{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5548 : ∀ a b c d : ℝ, (a + b) ^ 2 * (c ^ 2 + d ^ 2) ≥ (a * c + b * d) ^ 2   :=  by sorry

Source