lean_workbook_plus_15374

Proved

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

$x^{12}+x^{11}+x^{10}-5x^9+3x^8-7x^3+7\geq 3x^{11}+3x^8-5x^9-7x^3+7$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15374 : ∀ x : ℝ, x ^ 12 + x ^ 11 + x ^ 10 - 5 * x ^ 9 + 3 * x ^ 8 - 7 * x ^ 3 + 7 ≥ 3 * x ^ 11 + 3 * x ^ 8 - 5 * x ^ 9 - 7 * x ^ 3 + 7   :=  by sorry

Source

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

View graph