Lean proof search gains 32% by repairing failed tactics
Lean theorem provers can now repair rejected tactic steps instead of throwing them away, improving solve rates when sampling budgets are tight. The method feeds Lean’s precise compiler error into a repair model, retrying each failed step a bounded number of times; across tested candidate budgets, it delivered up to a 32% relative gain and solved 82 more theorems in a LeanDojo subset. The first repair attempt captured 84–96% of the total gain, while adding runtime.