Prove2Me

lean_workbook_plus_23699

Proved

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

Prove that (a+b)2(c+d)2+(a+c)2(b+d)2+(a+d)2(b+c)2≥3(a+b+c+d)(abc+bcd+cda+dab)(a+b)^2(c+d)^2+(a+c)^2(b+d)^2+(a+d)^2(b+c)^2\ge 3(a+b+c+d)(abc+bcd+cda+dab) where a,b,c,d>0a,b,c,d>0 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23699 (a b c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) : (a + b) ^ 2 * (c + d) ^ 2 + (a + c) ^ 2 * (b + d) ^ 2 + (a + d) ^ 2 * (b + c) ^ 2 >= 3 * (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