lean_workbook_plus_11733

Proved

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

Beregner Fibonacci-følgeren $F_n$ ved å bruke rekursion: $F_1 = F_2 = 1$ og $F_{n+1} = F_n + F_{n-1}$ . Finn $F_{8}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_11733 (F : ℕ → ℕ) (h₁ : F 1 = 1 ∧ F 2 = 1) (h₂ : ∀ n, F (n + 2) = F (n + 1) + F n) : F 8 = 21   :=  by sorry

Source