lean_workbook_plus_9012

Proved

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

Given the sequence $a_0=2,\ a_1=1,\ a_{n+2}=a_{n+1}+a_n$ . If $p$ is a prime and there exists $m$ such that $p|a_{2m}-2$ , prove that $p|a_{2m+1}-1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9012 (p : ℕ) (hp : p.Prime) (a : ℕ → ℕ) (h1 : a 0 = 2) (h2 : a 1 = 1) (h3 : ∀ n, a (n + 2) = a (n + 1) + a n) (h4 : ∃ m, p ∣ a (2 * m) - 2) : ∃ m, p ∣ a (2 * m + 1) - 1   :=  by sorry

Source

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

View graph