lean_workbook_plus_17079

Proved

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

Use homogenous-particular solution to recurrence relation. \n\nHomogenous Part \n\n $u_{n+2} =5u_{n+1} -6u_{n}$ \n\n $u^{n+2} =5u^{n+1} -6u^{n}$ \n\nThus, $u = 2$ or $u = 3$ \n\nHomogenous Part: $U_n = A(2)^n + B(3)^n$ \n\n

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17079 : ∃ A B : ℝ, ∀ n : ℕ, (A * 2 ^ n + B * 3 ^ n) = (5 * (A * 2 ^ (n - 1) + B * 3 ^ (n - 1)) - 6 * (A * 2 ^ (n - 2) + B * 3 ^ (n - 2)))   :=  by sorry

Source

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

View graph