lean_workbook_plus_17746

Disproved

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

Ugly way: $(a-b)^2(2a^6+5a^4b^2+4a^2b^4+b^6+10a^5b+15a^3b^3+5ab^5+26a^3b^2+13ab^4+27ab^3) \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17746 : ∀ a b : ℝ, (a - b) ^ 2 * (2 * a ^ 6 + 5 * a ^ 4 * b ^ 2 + 4 * a ^ 2 * b ^ 4 + b ^ 6 + 10 * a ^ 5 * b + 15 * a ^ 3 * b ^ 3 + 5 * a * b ^ 5 + 26 * a ^ 3 * b ^ 2 + 13 * a * b ^ 4 + 27 * a * b ^ 3) ≥ 0   :=  by sorry

Source

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

View graph