lean_workbook_plus_76771

Disproved

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

Prove that $12(x^{2}-xy+y^{2})a^{2}+3(4x^{3}+5x^{2}y-9xy^{2}+4y^{3})a+4x^{4}+5x^{3}y-9xy^{3}+4y^{4}\geq0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_76771 : ∀ x y a : ℝ, 12 * (x ^ 2 - x * y + y ^ 2) * a ^ 2 + 3 * (4 * x ^ 3 + 5 * x ^ 2 * y - 9 * x * y ^ 2 + 4 * y ^ 3) * a + 4 * x ^ 4 + 5 * x ^ 3 * y - 9 * x * y ^ 3 + 4 * y ^ 4 ≥ 0   :=  by sorry

Source

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

View graph