RAF: A Repair-Augmented Framework for LLM-Generated Lean Proofs

Large language models (LLMs) are increasingly used to generate complete formal proofs that can be verified by proof assistants such as Lean. However, successful verification requires knowledge of the target formal environment, and errors in generated proofs may exceed the capabilities of any single repair strategy. We present RAF, a training-free pipeline that combines external formal knowledge with complementary repair strategies for whole-proof generation in Lean 4. By retrieving relevant library declarations before generation, RAF provides explicit knowledge of available theorems and their signatures. After generation, RAF combines repair strategies with different repair boundaries to address complementary failure cases. We introduce lightweight sorrification, a diagnostic-guided strategy that localizes failing proof regions while preserving surrounding proof content, providing an alternative to broader repair strategies. The resulting proof obligations are addressed through local tactic repair, and only proofs verified by Lean without unresolved placeholders are counted as complete. Experiments across four LLMs on miniF2F show that RAF improves proof completion by at least 5% over the baseline repair pipeline, supporting the value of complementary repair within a knowledge-augmented proof generation pipeline.