Prove2Me

lean_workbook_plus_9034

Proved

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

The polynomial equals x4+x3+94x2+x+1−54x2=(x2+12x+1)2−(52x)2x^4+x^3+\frac{9}{4}x^2+x+1-\frac{5}{4}x^2=\left(x^2+\frac{1}{2}x+1\right)^2-\left(\frac{\sqrt{5}}{2}x\right)^2 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9034 : ∀ x : ℂ, x^4 + x^3 + (9 / 4) * x^2 + x + 1 - (5 / 4) * x^2 = (x^2 + (1 / 2) * x + 1)^2 - ((Real.sqrt 5 / 2) * x)^2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph