LeanPolish: Verified Supervision for Lean Proof Compression
Verified proof edits offer a natural source of supervision for improving language-model-generated Lean proofs. Yet verification establishes that an edit is correct, not that its training signal is free of search artifacts.
arXiv cs.LG2 min read