lean_workbook_plus_55606

Proved

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

By simple calculation, we get: $(x^2-3x-2)^2-3(x^2-3x-2)-2-x=(x^2-4x-2) (x^2-2x-4)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55606  (x : ℝ) :
  (x^2 - 3 * x - 2)^2 - 3 * (x^2 - 3 * x - 2) - 2 - x =
    (x^2 - 4 * x - 2) * (x^2 - 2 * x - 4)   :=  by sorry

Source

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

View graph