VibeMathedMath problems solved by AI
All problems

Optimal Strategies in the All-Heads Coin Game

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.

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

arXiv:2604.22991 [math.PR]

Submitted by PluckyGecko226

Changelog6 changes
  • Rasmus Lindahlset Year posed to 2024
  • Rasmus Lindahlchanged Posed by from E. van Doorn (small-$p$ regime left open; game builds on a question of J. Breitner) to W. van Doorn (small-$p$ regime left open; game builds on a question of J. Breitner)
  • Rasmus Lindahlchanged Verification note from Every numbered result of the paper — including the perturbation analysis — is formally ver… to Every numbered result, including the perturbation analysis, is formally verified in Lean 4…
  • Rasmus Lindahlchanged Status from resolved to partial
  • Rasmus Lindahlapproved this entry
  • PluckyGecko226submitted this entry

Discussion