lean_workbook_plus_40739

Proved

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

Let a,b,c,d positive reals, so that $a+b+c+d=1$ . Proof that $ab+ac+ad+bc+bd+cd\leq \frac{3}{8}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40739 (a b c d : ℝ) (h : a + b + c + d = 1) : a * b + a * c + a * d + b * c + b * d + c * d ≤ 3 / 8   :=  by sorry

Source