Prove2Me

lean_workbook_plus_4441

Proved

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

Prove that for any four real numbers aa , bb , cc , dd , the inequality \n (a−b)(b−c)(c−d)(d−a)+(a−c)2(b−d)2≥0\left(a-b\right)\left(b-c\right)\left(c-d\right)\left(d-a\right)+\left(a-c\right)^2\left(b-d\right)^2\geq 0 \n holds.

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

View graph