ProbXiv
sign in
machine only

Optimal Strategies in the All-Heads Coin Game

Everything below was recorded by a tool. No person has reviewed it, endorsed it, or written a word about it — so nothing here has been verified by anybody.

optimal-strategies-in-the-all-heads-coin-gameProbability & statisticsposed by W. van Doorn (small-$p$ regime left open; game builds on a question of J. Breitner), 2024recorded: partial

1 attempt · 1 machine check · no person has looked

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, nwn,pn\mapsto w_{n,p} is strictly increasing, and W(p)=limnwn,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 δ=12p\delta=\tfrac12-p gives a closed-form description: the deficit satisfies 12wn,1/2δδcn\tfrac12-w_{n,1/2-\delta}\approx\delta c_n, where cnc_n obeys a linear recursion for n7n\ge7 with limit L1.7035L\approx1.7035, and to first order the optimal-value sequence has a strict local minimum at n=5n=5 and no local maximum.

Context

A 2024 one-paper question growing out of a recreational puzzle, with no literature beyond the paper that posed it.

People

no project yet · nobody looking

Projects

none yet

Nobody is running a project on this. A project is a stated goal, a thread, and one thing somebody else could do. It takes a title, one sentence on what would count as progress, and that one task.

begin a project on this problem →

Interest

nobody looking

Nobody has said they are looking at this. A mark here is a statement about you, not a claim on the problem: you set it, you clear it, and it blocks nobody.

Attempts

1 attempt

No person has examined this. There is 1 attempt here and 1 machine check recorded against it. A machine check is a judgement recorded by a tool: no account is credited for it, nobody has put their name to it, and it is not verification by a person. Saying whether the mathematics holds is the most useful thing anybody can do on this page.

review this attempt

  • #1

    Attempt 1

    proof attemptClaude Opus 4.6 / 4.7 / 4.8 with Peter Pfaffelhuber ·
    AI involvement
    ai co developed
    a person and a model developed the result together.
    models
    Claude Opus 4.6, 4.7, 4.8
    people
    Peter Pfaffelhuber

    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.

    Reviews

    0 human reviews · 1 machine check

    No person has reviewed this attempt. 1 machine check below — a machine check is not human verification.

    • Machine check · not human verification

      machine: correct

      Recorded from Lean ·

      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.

      No ProbXiv account is credited for this check. Nobody has put their name to it, so it carries no personal accountability and does not count as verification by a person.

    Endorsements

    0 endorsements

    No one has endorsed this attempt. An endorsement is a person stating that they checked this version and believe it is correct. None has been recorded — which is information, not an omission.

    Discussion of this attempt

    no comments

Discussion

no comments

Nothing has been said about this problem yet. Discussion is for questions about the statement, pointers to prior work and objections to an attempt. It is not review: a review is a verdict recorded against one version of one attempt, and it is counted separately.

Reading every thread is open to everyone. Posting needs an account with posting rights — sign in to check yours.