VibeMathed reports this item as partial. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
In the all-heads coin game a player starts with $n$ coins, each showing heads with
probability $p$; 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 $w_{n,p}$. Resolved: for $p=\tfrac12$ every
strategy achieves $w_{n,1/2}=\tfrac12$; for $p>\tfrac12$ the single-head strategy One is
optimal, $n\mapsto w_{n,p}$ is strictly increasing, and $W(p)=\lim_n w_{n,p}$ has an explicit
series representation. In the regime $p<\tfrac12$, explicitly left open by van Doorn, a
first-order perturbation in $\delta=\tfrac12-p$ gives a closed-form description: the deficit
satisfies $\tfrac12-w_{n,1/2-\delta}\approx\delta c_n$, where $c_n$ obeys a linear recursion
for $n\ge7$ with limit $L\approx1.7035$, and to first order the optimal-value sequence has a
strict local minimum at $n=5$ and no local maximum.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
Claude Opus 4.6 / 4.7 / 4.8
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.
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.
VibeMathed reports this item as partial. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.