The two real roots of a quadratic

Proved

WorkbookTyped.plus_43951

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbookrepaired-variable-declarationssource-checked

Solve for $x$ : $x^2 - 2x - 1 = 0$

Declaration repair: Added the explicit real binder (x : ℝ). The original formula already uses Real.sqrt, which fixes the intended real equation once its variable is declared.

Source: InternLM Lean-Workbook, record lean_workbook_plus_43951 (Apache-2.0). Original malformed declaration. This record proves the corrected statement.

Preamble

import Mathlib

Formal statement

theorem WorkbookTyped.plus_43951 (x : ℝ) : x^2 - 2*x - 1 = 0 ↔ x = 1 + Real.sqrt 2 ∨ x = 1 - Real.sqrt 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_43951; explicit variable-declaration repair; Apache-2.0

View graph