lean_workbook_plus_60748

Proved

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

Finally the number of good sequences is $3^{1959}\cdot \dfrac{3^{64}+1}{2}-2^{2023}+2^{2022}=\boxed {\dfrac{3^{2023}+3^{1959}}{2}-2^{2022}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60748 :
  (3^1959 * (3^64 + 1) / 2 - 2^2023 + 2^2022) = (3^2023 + 3^1959) / 2 - 2^2022   :=  by sorry

Source