Foreign Exchange and Proof Diversity: Which Failures to Borrow and Which Retries to Buy

After a Lean prover fails a theorem, what should its next attempt see, and how much computation should it get? We study both questions with frozen, 4-bit provers on selected miniF2F theorems. Goedel-Prover-V2 recovers far more often when shown another prover’s whole failed reply than its own: 21/84 versus 6/84 verified retries with DeepSeek-Prover-V2 as the donor (Holm $p=.014$), and 25/68 versus 4/68 with Kimina-Prover (Holm $p=.0015$). Its own failed reply, which it mostly copies back, is also worse than a fresh retry, while foreign replies are almost never copied; whether a foreign failure beats a fresh retry remains unresolved. Telling the model that its own reply came from another prover does not help. How a failure was made matters too: shown as code, heavily corrupted correct proofs are recovered from far more often than genuine failures (37/84 versus 21/84, Holm $p=.024$), so repair benchmarks built on corrupted proofs can overstate recovery. Finally, failure types are more useful for budgeting than as prompt text: in our earlier experiments, failure-aware retry allocation saved 27.5–33.9% of retry tokens in the primary draw order, and a targeted output cap saved 11.2–13.3% of measured GPU energy, without losing solves. Which failed proof to show and how much compute to spend are separate decisions, and each should be judged against a fresh retry. Confirmatory analysis plans for the new studies were frozen before generation.