lean_workbook_plus_81683

Disproved

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

Prove that $2(a^2+b^2+c^2)^2\geq 27-3(a^2b+b^2c+c^2a)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source