lean_workbook_plus_15001

Disproved

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

prove that: \n $(a+b+c+d)^4+16(a-b)(b-c)(c-d)(d-a)-4(a+b+c+d)^2(c+a)(b+d)\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15001 : ∀ a b c d : ℝ, (a + b + c + d)^4 + 16 * (a - b) * (b - c) * (c - d) * (d - a) - 4 * (a + b + c + d)^2 * (c + a) * (b + d) ≥ 0   :=  by sorry

Source

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

View graph