lean_workbook_plus_58461

Disproved

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

Lemma 2.\n $(a^3+b^3+c^3)(ab+bc+ca)^2\geq 3abc(a^2+b^2+c^2)^2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58461 : ∀ a b c : ℝ, (a^3 + b^3 + c^3) * (a * b + b * c + c * a)^2 ≥ 3 * a * b * c * (a^2 + b^2 + c^2)^2   :=  by sorry

Source