Bounded compiler-guided repair improves tactic-level proof search in Lean 4
The paper introduces a bounded, online step-level repair that samples K candidate tactics per proof step and, when a tactic is rejected, feeds the compiler error message to a pretrained repair model to fix that step in place up to R times. On a 1,990-theorem subset of the LeanDojo benchmark the method yields up to a 32% relative improvement (82 additional theorems solved) across tested K∈{1,3,5,8}, replicates on the Lean Workbook benchmark (nearly doubling solve rate), and shows gains concentrate on shallow tactic-execution failures at the expense of predictable extra runtime.