lean_workbook_plus_17478

Proved

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

The first ten $a(i)$ are $1, 4, 22, 316, 6976, 373024, 32252032, 6619979776, 2253838544896, 1810098020122624$ . We see that when $10\geq n\geq 5$ , $a(n)=0 \;mod\; 8$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17478 (n : ℕ) (f : ℕ → ℕ) (hf: f 1 = 1 ∧ f 2 = 4 ∧ f 3 = 22 ∧ f 4 = 316 ∧ f 5 = 6976 ∧ f 6 = 373024 ∧ f 7 = 32252032 ∧ f 8 = 6619979776 ∧ f 9 = 2253838544896 ∧ f 10 = 1810098020122624): (n >= 5 ∧ n <= 10) → f n % 8 = 0   :=  by sorry

Source

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

View graph