Prove2Me

A sixth-degree nonnegative polynomial

Proved
WorkbookSource.problem_12277

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

lean-workbooksource-checked

Simplify and prove the inequality after squaring both sides:

(a−1)2(9a4−84a3+310a2−580a+601)≥0(a-1)^2(9a^4-84a^3+310a^2-580a+601)\geq0

Source: InternLM Lean-Workbook, record lean_workbook_12277 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_12277 : ∀ a : ℝ, (a - 1) ^ 2 * (9 * a ^ 4 - 84 * a ^ 3 + 310 * a ^ 2 - 580 * a + 601) ≥ 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_12277; Apache-2.0

View graph