lean_workbook_plus_60463

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} = 2$ and ${u_{n + 1}} = 9u_n^3 + 3{u_n}, \forall n \in \mathbb{N}*$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60463 (u : ℕ → ℕ) (h : u 1 = 2) (h' : ∀ n, u (n + 1) = 9 * u n ^ 3 + 3 * u n) : ∃ f : ℕ → ℕ, ∀ n, u n = f n   :=  by sorry

Source