lean_workbook_plus_44185

Proved

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

Let $T_k$ be the expected remaining time in the process, conditioned on the last $k$ flips having been heads. Note that $T_3=0.$ Considering what happens on the next flip gives us the following system of equations: $T_0=1+\frac12T_0+\frac12T_1$ $T_1=1+\frac12T_0+\frac12T_2$ $T_2=1+\frac12T_0$ This $3\times 3$ linear system can be solved readily. We get that $T_2=8,T_1=12,$ and $T_0=14.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_44185  (t0 t1 t2 : ℝ)
  (h0 : t0 = 1 + t0 / 2 + t1 / 2)
  (h1 : t1 = 1 + t0 / 2 + t2 / 2)
  (h2 : t2 = 1 + t0 / 2) :
  t2 = 8 ∧ t1 = 12 ∧ t0 = 14   :=  by sorry

Source

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

View graph