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

Haotian Deng, Chris Farber, Sonal Narasimha +2

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 samp…