lean_workbook_plus_11269

Proved

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

$P(k)$ : For some natural number $k$ , $a_n = a_{2^k+k-2} = (2^{k-1})^2 = m^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11269 (n : ℕ) (a : ℕ → ℕ) (h₁ : ∃ k : ℕ, a n = a (2^k + k - 2) ∧ a (2^k + k - 2) = (2^(k-1))^2) : ∃ m : ℕ, a n = m^2   :=  by sorry

Source

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

View graph