Proof Yahtzee: From Prompting to Scheduling — Failure Signals for Token-Efficient Retries in Frozen Lean Provers

Verifier-gated retries are a simple, low-overhead form of test-time scaling for a frozen, locally served Lean 4 prover: only theorems still lacking a verified proof receive more tokens. We report a controlled study in a resource-constrained environment (Q4KM-quantized provers, a single consumer GPU), centered on Goedel-Prover-V2-8B and extended to Kimina-Prover and DeepSeek-Prover, with one organizing finding: first-attempt failure signals did not detectably improve retries when placed in the attempt-blind retry prompts we evaluated, yet the same signals predict a roughly 20x spread in retry success per completion token and support cheaper allocation of repeated samples. On the prompting side, three apparent wins, one nominally significant (McNemar p=0.039), failed matched-seed replication or pre-specified prospective tests (p=0.549 at matched seeds); across 19 retry draws, no tested prompt policy robustly beat plain reseeded resampling, whose four-draw union alone lifted the baseline from 119/202 to 146/202. On the allocation side, a deliberately elementary frozen rule set built on the failure classes (never retry timeouts, cap truncation retries, order the rest by measured retryability) was evaluated prospectively under a pre-specified protocol on 40 held-out stage-one failures: the rules solved the same 14 theorems as sequential resampling using 27.5% fewer retry-stage tokens and were never more than one solve behind under draw reordering. The result replicated in a second pre-specified seed block at 33.9% savings, with a bootstrap interval excluding zero, whereas the first block’s interval crosses zero. Component ablations on both blocks attribute the realized savings chiefly to the two coarse clauses (suppressing timeout retries, capping truncation retries), and a calibrated learned scheduler did not beat the rules. The frozen rules also transfer without tuning: two pre-specified seed blocks on Kimina-Prover’s failure pool reach parity at zero deficit with 26.7% and 44.2% primary-ordering savings, while on DeepSeek-Prover, whose failure pool contains neither timeouts nor truncations, the rules match uniform’s spend on the primary ordering and in the median. Across these three frozen policies, savings were observed when the failure pool contained costly budget classes. With caching disabled, each recorded (prompt, seed) request is byte-reproducible, and allocation policies are compared by exact paired replay over identical recorded attempts; the replay methodology, all draws, and the negative results are released in full in an anonymized repository.