Prove2Me

lean_workbook_plus_44257

Disproved

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

Prove the given statement about the remainder of ana_n when divided by 4: a1≡1;a2≡1;a3≡2;for n⩾4 even, an≡1(mod4);for n⩾5 odd, an≡0(mod4).a_1\equiv 1; a_2\equiv 1; a_3\equiv 2; \text{for }n\geqslant 4 \text{ even, } a_n\equiv 1\pmod 4; \text{for }n\geqslant 5 \text{ odd, } a_n\equiv 0\pmod 4.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44257 (a : ℕ → ℕ) (a1 : a 0 = 1) (a2 : a 1 = 1) (a3 : a 2 = 2) (a_rec : ∀ n, a (n + 3) = a (n + 1) + a n) : ∀ n, (n ≥ 4 ∧ Even n → a n ≡ 1 [ZMOD 4]) ∧ (n ≥ 5 ∧ Odd n → a n ≡ 0 [ZMOD 4])   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph