Prove2Me

lean_workbook_plus_59599

Proved

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

Let α=k+3+k−12\alpha = \frac{\sqrt{k+3}+\sqrt{k-1}}{2} and β=k+3−k−12\beta = \frac{\sqrt{k+3}-\sqrt{k-1}}{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59599 (α β : ℝ) (k : ℝ) : α = (Real.sqrt (k + 3) + Real.sqrt (k - 1)) / 2 ∧ β = (Real.sqrt (k + 3) - Real.sqrt (k - 1)) / 2 ↔ α + β = Real.sqrt (k + 3) ∧ α - β = Real.sqrt (k - 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph