lean_workbook_plus_43252

Disproved

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

Given the recursive sequence defined by $a_1 = 1$ , $a_2 = 1$ , and $a_{n+2} = a_{n+1} + a_n$ for $n \geq 1$ , and the sequence $b_n = a_{n+1} + a_{n+2}$ for $n \geq 1$ , prove that $b_i = 0$ for some $i$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43252 (a : ℕ → ℕ) (b : ℕ → ℕ) (h₁ : a 1 = 1) (h₂ : a 2 = 1) (h₃ : ∀ n, a (n + 2) = a (n + 1) + a n) (h₄ : ∀ n, b n = a (n + 1) + a (n + 2)) : ∃ i, b i = 0   :=  by sorry

Source

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

View graph