Automated theorem provers often rely on sampling language models to generate tactics, while interactive proof assistants such as Lean return a precise error message for each failed step, information that pure sampling discards. To address this, we introduce a bounded, online step‑level repair module. At each step the search samples $K$ candidate tactics and repairs a failed tactic at most $R$ times. Instead of discarding the failed tactics, we feed the compiler’s error message to a pretrained repair model to fix the rejected step in place. Experiments show that across all candidate budgets $K\in\{1,3,5,8\}$ this approach improves the solve rate over a sampling‑only baseline, achieving up to a $32\%$ relative gain and solving $82$ additional theorems on a $1{,}990$‑theorem subset of the LeanDojo benchmark. Repair is not free: it trades extra runtime for reachable proofs, but the trade‑off is predictable—repair pays most when sampling is constrained, its return is front‑loaded, with the first repair attempt capturing $84\text{--}96\%$ of the total gain, and the gain comes almost entirely from shallow tactic‑execution failures rather than structural errors such as type mismatches. This targeted repair also replicates successfully on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions.
Review