Optimal strategies in the all-heads coin game
Peter Pfaffelhuber
math.PR
Apr 24, 2026 · v2
TL;DR
Every numbered result is machine-checked in a sorry-free Lean 4/Mathlib formalization, written with Claude's assistance and published in a public repository.
Abstract
We study a sequential coin-flipping game: a player starts with $n$ coins, each heads with probability $p$, and in each round flips all remaining coins and must set aside at least one head, losing if none shows. The player wins once all coins have been set aside. The optimal winning probability $w_{n,p}$ obeys a Bellman equation with a nonlinear suffix-maximum operator. For $p=\tfrac12$ every strategy achieves $w_{n,1/2}=\tfrac12$. For $p>\tfrac12$ the strategy \One{} (set aside a single head) is optimal, $n\mapsto w_{n,p}$ is strictly increasing, and the limit $W(p):=\lim_n w_{n,p}$ has an explicit series representation with $p\le W(p)<1$. For $p<\tfrac12$ near $\tfrac12$ we give a first-order perturbation expansion in $δ:=\tfrac12-p$: the deficit satisfies $\tfrac12-w_{n,\,1/2-δ}\approxδ\,c_n$, where $c_n$ obeys a linear recursion for $n\ge7$ with limit $L\approx1.7035$. To first order the optimal-value sequence has a strict local minimum at $n=5$ and no local maximum.
Problem
A player flips n coins, each heads with probability p, and in each round must set aside at least one head, losing if none shows. The goal is to characterize the optimal winning probability w_{n,p}, which satisfies a Bellman equation with a nonlinear suffix-maximum operator.
Approach
For p=1/2 and p>1/2 the analysis uses strong induction and collapse of the suffix-maximum, giving a linear recursion and a series formula for the limit W(p). For p slightly below 1/2, a first-order perturbation in δ=1/2-p yields a deficit coefficient c_n obeying a linear recursion for n≥7. All numbered results are formalized in Lean 4/Mathlib with Claude's help, and numerical experiments use exact Bellman recursion.
Results
For p=1/2 every strategy that accepts the immediate win gives w=1/2. For p>1/2 setting aside one head is optimal and w_{n,p} is strictly increasing, with p≤W(p)<1. Near p=1/2, c_n converges to L≈1.7035, and to first order w has a strict local minimum at n=5 and no local maximum; the Lean proofs use no sorry and only the standard axioms.
