Prove2Me

lean_workbook_plus_15826

Disproved

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

We can solve this by recursion. \nLet f(n) be the number of ways to arrange the coins after n flips. \nIf the previous one was a tail, then there are f(n-1) ways to do it. \nIf the previous one was a head, then the next one has to be a head, so there are f(n-2) ways to do it. \nf(n)=f(n-1)+f(n-2). We can easily see f(0)=1 and f(1)=1, so we can solve from there for f(9) to get the answer is 89.\boxed{89}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15826  (f : ℕ → ℕ)
  (h₀ : f 0 = 1)
  (h₁ : f 1 = 1)
  (h₂ : ∀ n, f (n + 2) = f (n + 1) + f n) :
  f 9 = 89   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph