lean_workbook_plus_48710

Proved

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

Prove that $a^4 + b^4 + c^4 + a^2b^2 + b^2c^2 + c^2a^2 \geq a^3b + ab^3 + b^3c + bc^3 + c^3a + ca^3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48710 : ∀ a b c : ℝ, a ^ 4 + b ^ 4 + c ^ 4 + a ^ 2 * b ^ 2 + b ^ 2 * c ^ 2 + c ^ 2 * a ^ 2 ≥ a ^ 3 * b + a * b ^ 3 + b ^ 3 * c + b * c ^ 3 + c ^ 3 * a + c * a ^ 3   :=  by sorry

Source

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

View graph