Prove2Me

lean_workbook_plus_31326

Proved

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

Given x5−x3+x=ax^{5}-x^{3}+x=a, prove (x−1)2(x2+x3+1)(x2−x3+1)⩾0(x-1)^{2}(x^{2}+x\sqrt{3}+1)(x^{2}-x\sqrt{3}+1)\geqslant 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31326 (x a : ℝ) (h : x^5 - x^3 + x = a) :
  (x - 1)^2 * (x^2 + x * Real.sqrt 3 + 1) * (x^2 - x * Real.sqrt 3 + 1) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph