Optimal Strategies in the All-Heads Coin Game
Statement
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.
Record
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
Peter Pfaffelhuber, using Claude Opus 4.6, 4.7, 4.8That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.
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 and producing numerical scripts, with every edit reviewed by the author.
Machine-checked by Lean on #1 · not a person
lean: correctLeanscope Lean formalization of the result
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), nonative_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.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.