lean_workbook_plus_80870

Proved

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

Prove that the sequence defined recursively by $a_1=0,a_2=1$ and $a_{4n} = 1 -a_{n+1}$ , $a_{4n+2}=a_{n+2}$ , $a_{2n+1} = a_n$ is not periodic.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_80870 (a : ℕ → ℤ) (a1 : a 0 = 0) (a2 : a 1 = 1) (a_rec : ∀ n, a (4 * n) = 1 - a (n + 1) ∧ a (4 * n + 2) = a (n + 2) ∧ a (2 * n + 1) = a n) : ¬ ∃ n, 0 < n ∧ ∀ k, a k = a (k + n)   :=  by sorry

Source

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

View graph