lean_workbook_plus_53170

Proved

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

Prove that $(a+b) (c+d)(a+d)(b+c)\ge (a+b+c+d) ( a b c + b c d + c d a + d a b)$ , $(a+d)(b+c)(a+c)(b+d)\ge (a+b+c+d) ( a b c + b c d + c d a + d a b)$ , and $(a+c)(b+d)(a+b) (c+d)\ge (a+b+c+d) ( a b c + b c d + c d a + da b)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53170 (a b c d : ℝ) : (a+b) * (c+d) * (a+d) * (b+c) ≥ (a+b+c+d) * (a * b * c + b * c * d + c * d * a + d * a * b) ∧ (a+d) * (b+c) * (a+c) * (b+d) ≥ (a+b+c+d) * (a * b * c + b * c * d + c * d * a + d * a * b) ∧ (a+c) * (b+d) * (a+b) * (c+d) ≥ (a+b+c+d) * (a * b * c + b * c * d + c * d * a + d * a * b)   :=  by sorry

Source

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

View graph