lean_workbook_plus_73173

Proved

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

Prove that: $F_n^2+F_{n+4}^2=F_{n+1}^2+4F_{n+2}^2+F_{n+3}^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73173 (n : ℕ) (f : ℕ → ℕ) (h : ∀ n, f (n + 2) = f n + f (n + 1)) : (f n)^2 + (f (n + 4))^2 = (f (n + 1))^2 + 4 * (f (n + 2))^2 + (f (n + 3))^2   :=  by sorry

Source

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

View graph