A two-variable sixth-degree polynomial is nonnegative

Proved

WorkbookSource.base_14272

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Prove that $28a^6 + 44a^5v + 20a^4v^2 - 10a^3v^3 - 2a^2v^4 + 7av^5 + 4v^6 \geq 0$ for all non-negative real numbers $a$ and $v$ .

Source: InternLM Lean-Workbook, record lean_workbook_14272 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_14272 (a v : ℝ) (ha : 0 ≤ a) (hv : 0 ≤ v) : 28 * a ^ 6 + 44 * a ^ 5 * v + 20 * a ^ 4 * v ^ 2 - 10 * a ^ 3 * v ^ 3 - 2 * a ^ 2 * v ^ 4 + 7 * a * v ^ 5 + 4 * v ^ 6 ≥ 0  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_14272; Apache-2.0

View graph