Prove2Me

lean_workbook_plus_30628

Proved

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

Let a,b,c,d a,b,c,d are real numbers,prove that: (b2+c2+d2+a2)2≥b2(b+d)(c+a)+c2(c+a)(b+d)+d2(b+d)(c+a)+a2(c+a)(b+d).(b^2+c^2+d^2+a^2)^2 \geq b^2(b+d)(c+a)+c^2(c+a)(b+d)+d^2(b+d)(c+a)+a^2(c+a)(b+d).

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_30628 (a b c d : ℝ) : (b^2+c^2+d^2+a^2)^2 >= b^2 * (b+d) * (c+a) + c^2 * (c+a) * (b+d) + d^2 * (b+d) * (c+a) + a^2 * (c+a) * (b+d)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph