ProbXiv
sign in
Problem archiveProblem record

Statement

In the all-heads coin game a player starts with nn coins, each showing heads with probability pp; 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 wn,pw_{n,p}. Resolved: for p=12p=\tfrac12 every strategy achieves wn,1/2=12w_{n,1/2}=\tfrac12; for p>12p>\tfrac12 the single-head strategy One is optimal, n↦wn,pn\mapsto w_{n,p} is strictly increasing, and W(p)=lim⁡nwn,pW(p)=\lim_n w_{n,p} has an explicit series representation. In the regime p<12p<\tfrac12, explicitly left open by van Doorn, a first-order perturbation in δ=12−p\delta=\tfrac12-p gives a closed-form description: the deficit satisfies 12−wn,1/2−δ≈δcn\tfrac12-w_{n,1/2-\delta}\approx\delta c_n, where cnc_n obeys a linear recursion for n≥7n\ge7 with limit L≈1.7035L\approx1.7035, and to first order the optimal-value sequence has a strict local minimum at n=5n=5 and no local maximum.

Record

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. proof attempt · #1

    Peter Pfaffelhuber, using Claude Opus 4.6, 4.7, 4.8

    That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.

    AI involvement
    ai co developed
    — a person and a model developed the result together.

    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.

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope 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), 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.

    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 in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.