lean_workbook_plus_9391

Disproved

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

$\Leftrightarrow 12(x-y)^2(x^4+y^4+x^3y+xy^3+x^2y^2)-13x^2y^2(x-y)^2 \ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9391 : ∀ x y : ℝ, 12*(x-y)^2*(x^4+y^4+x^3*y+x*y^3+x^2*y^2) - 13*x^2*y^2*(x-y)^2 ≥ 0   :=  by sorry

Source