lean_workbook_plus_74285

Disproved

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

Therefore, we have $p_n = \frac{1}{6} ( 1+p_{n-1})$ . Note that $p_1 = \frac{1}{6}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74285  (p : ℕ → ℚ)
  (h₀ : p 1 = 1 / 6)
  (h₁ : ∀ n, p (n + 1) = 1 / 6 * (1 + p n)) :
  p 5 = 33 / 38   :=  by sorry

Source