lean_workbook_plus_40051

Proved

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

Find the closed form of the sequence defined by $U_1=U_2=1$ and $U_{2k+1}=3U_{2k}+6U_{2k-1}, U_{2k+2}=3U_{2k+1}-6U_{2k}$ for $k \ge 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40051 (U : ℕ → ℤ) (h₁ : U 1 = 1) (h₂ : U 2 = 1) (h₃ : ∀ k, U (2 * k + 1) = 3 * U (2 * k) + 6 * U (2 * k - 1)) (h₄ : ∀ k, U (2 * k + 2) = 3 * U (2 * k + 1) - 6 * U (2 * k)) : ∃ f : ℕ → ℤ, ∀ n, U n = f n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph