lean_workbook_plus_46825

Disproved

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

In the third: \n $x^2 - 7 = x - 1\implies x^2 - x - 8 = 0\implies x = \frac {1\pm\sqrt {33}}{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46825  (x : ℝ)
  (h₀ : x^2 - 7 = x - 1) :
  x^2 - x - 8 = 0   :=  by sorry

Source