lean_workbook_plus_4583

Disproved

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

Prove that $a^{3}b+b^{3}c+c^{3}a\ge a^{2}b^{2}+b^{2}c^{2}+c^{2}a^{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4583 : ∀ a b c : ℝ, a ^ 3 * b + b ^ 3 * c + c ^ 3 * a >= a ^ 2 * b ^ 2 + b ^ 2 * c ^ 2 + c ^ 2 * a ^ 2   :=  by sorry

Source