lean_workbook_plus_62330

Proved

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

Denote $p(x)$ to be the probability of no consecutive tails after $x$ coin flips. When $x\ge 2$ , $p(x)=\frac{1}{2}p(x-1)+\frac{1}{2}\times\frac{1}{2}p(x-2)$ . Now we can build a chart and get to $6$ coin flips. $p(0)=1, p(1)=1, p(2)=\frac{1}{2}\times1+\frac{1}{4}\times1=\frac{3}{4}, p(3)=\frac{5}{8}, p(4)=\frac{8}{16}, p(5)=\frac{13}{32}, p(6)=\frac{21}{64}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62330  (p : ℕ → ℚ)
  (h₀ : p 0 = 1)
  (h₁ : p 1 = 1)
  (h₂ : ∀ x, p (x + 2) = 1 / 2 * p (x + 1) + 1 / 4 * p x) :
  p 6 = 21 / 64   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph