lean_workbook_plus_8013

Disproved

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

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

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source