LeanPolish: Verified Supervision for Lean Proof Compression
arXiv:2609.38384v1 Announce Type: new Abstract: Verified proof edits offer a natural source of supervision for improving language-model-generated Lean proofs. Yet verification establishes that an edit