lean_workbook_plus_37211
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_37211 (S : ℕ → ℕ) (h : S 2023 = (3 * 2 ^ 2023 + 1) / 7) : S 2023 = 2 ^ 2022 - (2 ^ 2022 - 1) / (2 ^ 3 - 1) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_37211 (S : ℕ → ℕ) (h : S 2023 = (3 * 2 ^ 2023 + 1) / 7) : S 2023 = 2 ^ 2022 - (2 ^ 2022 - 1) / (2 ^ 3 - 1) := by sorry