The greatest common divisor of two Fibonacci numbers

Proved

WorkbookRestored.plus_41195

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

lean-workbookrestored-importssource-checked

For natural numbers $n,m$ , $\gcd(F_n,F_m)=F_{\gcd(n,m)}$ , where $F_0=0$ , $F_1=1$ and $F_{r+2}=F_r+F_{r+1}$ .

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

Preamble

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

Formal statement

theorem WorkbookRestored.plus_41195 (n m : ℕ) : Nat.gcd (Nat.fib n) (Nat.fib m) = Nat.fib (Nat.gcd n m)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_41195; original Prove2Me node 62fdbf73-c359-4363-ad01-cfb6184d1302; Apache-2.0

View graph