A sum of two consecutive Fibonacci squares

Proved

WorkbookRestored.plus_9802

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For the Fibonacci sequence with $F_0=0$ and $F_1=1$ , every natural number $n$ satisfies

F_n^2+F_{n+1}^2=F_{2n+1}.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_9802 (Apache-2.0).

Preamble

import Mathlib.Data.Nat.Fib.Basic
open Nat

Formal statement

theorem WorkbookRestored.plus_9802 (n : ℕ) : fib n ^ 2 + fib (n + 1) ^ 2 = fib (2 * n + 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_9802; original Prove2Me node 1e0209bc-c754-4f67-8176-ec0ed721360b; Apache-2.0

View graph