# Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

Preprint · Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue

- Archive id: arxiv:2610.26942
- Published: 2026-10-18
- arXiv: https://arxiv.org/abs/2610.26942
- Source URL: https://arxiv.org/abs/2610.26942
- PDF: https://arxiv.org/pdf/2610.26942
- Provenance: arxiv

## Abstract

Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples $K$ candidate tactics at each step and repairs a failed tactic at most $R$ times. Instead of discarding failed tactics, we feed the compiler's error message to a pretrained repair model to fix individual rejected steps in place. This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets ($K \\in \\{1,3,5,8\\}$), 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 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 successfully replicates on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.