The fourteenth Fibonacci number

Proved

WorkbookRestored.plus_49452

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

lean-workbookrestored-importssource-checked

The fourteenth Fibonacci number is $F_{14}=377$ , with $F_0=0$ , $F_1=1$ and $F_{n+2}=F_n+F_{n+1}$ .

Source: Lean-Workbook row lean_workbook_plus_49452 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

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

Formal statement

theorem WorkbookRestored.plus_49452 : fib 14 = 377   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_49452; immutable original Prove2Me node 48463b56-7ef9-4600-96ec-2ef8197e33ba

View graph