lean_workbook_plus_77702

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_77702  (x : ℝ)
  (h₀ : x^2 - 7 = x - 1) :
  x = (1 + Real.sqrt 33) / 2 ∨ x = (1 - Real.sqrt 33) / 2   :=  by sorry

Source