Optimal Strategies in the All-Heads Coin Game
In the all-heads coin game a player starts with coins, each showing heads with probability ; each round all remaining coins are flipped, the player must set aside at least one head (losing if none shows), and wins once all coins are set aside. Determine optimal strategies and the winning probability . Resolved: for every strategy achieves ; for the single-head strategy One is optimal, is strictly increasing, and has an explicit series representation. In the regime , explicitly left open by van Doorn, a first-order perturbation in gives a closed-form description: the deficit satisfies , where obeys a linear recursion for with limit , and to first order the optimal-value sequence has a strict local minimum at and no local maximum.
- Result
- Proved
- Status
- Partial result
- AI contribution
- AI co-developed
- Method
- Argument
- Field
- Markov decision processes
- Posed by
- W. van Doorn (small-$p$ regime left open; game builds on a question of J. Breitner)
- Year posed
- 2024
- Years open
- 2y
- Solved
- 2026-04-24
- Model
- Claude Opus 4.6 / 4.7 / 4.8
- Vendor
- Anthropic
- Collaborators
- Peter Pfaffelhuber
- Verification
- Lean-verified
- Publication
- Preprint
- Significance
- —
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
Per the paper's authorship disclosure: Claude (Anthropic; versions Opus 4.6, 4.7, 4.8), used interactively, produced the mathematical text, the numerical code, and the complete Lean 4/Mathlib formalization. The underlying ideas, choice of research question, the structuring of the joint induction, and the decision to formally verify are the author's; Claude's role was execution — drafting exposition, proposing and debugging Lean proof tactics, selecting Mathlib lemmas, producing numerical scripts — with every edit reviewed by the author.
Verification
Every numbered result, including the perturbation analysis, is formally verified in Lean 4 with Mathlib: no `sorry`, no custom axioms (only propext, Classical.choice, Quot.sound), no `native_decide`/`unsafe`. Trust surface is two files (`CoinsLean/Challenge.lean`, `CoinsLean/CoinsLean/Defs.lean`), independently checkable via the Lean comparator on the public repository; manuscript↔Lean map in Appendix A. arXiv preprint (v2, June 2026), not peer-reviewed. Status set to partially resolved (2026-08-02): p = 1/2 and p > 1/2 are fully resolved, but for p < 1/2 the paper gives only a first-order expansion in δ = 1/2 − p near 1/2, leaving the range of validity δ₀(n) open and the numerically observed local maxima outside its reach. Verification tier unchanged: the Lean checks what the paper claims, and the paper does not claim the full small-p regime.
Sources
Submitted by PluckyGecko226