Beyond Retry: A Budget-Controlled Ablation of Compiler Feedback for Lean Proof Repair

Formal theorem-proving agents frequently feed Lean compiler diagnostics back to language models after failed proof attempts. Yet existing improvements from compiler-guided repair do not establish which part of that feedback is responsible: semantic error information, a binary failure verdict, additional prompt context, or simply another opportunity to generate. We present a budget-controlled evaluation that isolates the informational value of compiler feedback in iterative Lean proof repair. Starting from 219 failed attempts of a public checkpoint (deepseek-ai/DeepSeek-Prover-V1.5-RL) on a version-pinned Lean 4 benchmark (LeanDojo Benchmark 4 (v10)), we compare four feedback conditions: full diagnostics, binary success/failure, no feedback, and length-matched non-diagnostic placebo text. All conditions use identical model checkpoints, theorem splits, decoding seeds, maximum generated tokens, prompt-length caps, and Lean verifier-call budgets; the primary comparisons are full diagnostics against the placebo and against the binary verdict, which differ from it only in the feedback text. At the pre-specified budget of 8 verifier calls and 3 seeds, the paired full-minus-placebo difference in solved rate is +0.9 percentage points (95% interval [-2.4, +4.0]) and the paired full-minus-binary difference is +1.2 ([-2.1, +4.4]); both intervals include zero. The secondary full-minus-none difference, which also changes the state context, is -9.9 ([-14.5, -5.3]): independent resampling from the same initial failure reached accepted proofs more often than any condition that showed the model its previous attempt. For this model and benchmark, the length-matched placebo and the binary verdict recover whatever the repair loop adds, and we find no evidence that diagnostic semantics add to retry and context effects at equal budgets. By checker-observable failure category, no bucket shows a primary difference whose interval excludes zero; bucket slices are descriptive. We release scripts, environment locks, prompts, seeds, raw per-attempt records and complete checker traces; one command regenerates every table and figure.