lean_workbook_plus_7074

Proved

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

Prove that $a^4 + b^4 + c^4 + d^4 + a^2b^2 + b^2c^2 + c^2d^2 + d^2a^2\geq 2 (a^3 b + b^3 c + c^3 d + a d^3)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7074 (a b c d : ℝ) : a ^ 4 + b ^ 4 + c ^ 4 + d ^ 4 + a ^ 2 * b ^ 2 + b ^ 2 * c ^ 2 + c ^ 2 * d ^ 2 + d ^ 2 * a ^ 2 ≥ 2 * (a ^ 3 * b + b ^ 3 * c + c ^ 3 * d + a * d ^ 3)   :=  by sorry

Source

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

View graph