Announcement_11

New preprint: LeanPolish: Verified Supervision for Lean Proof Compression. A neurosymbolic Lean 4 proof-compression method that records every verified edit, exposes the selection effects of search-generated supervision, and shows when learning from it helps beyond symbolic search. Code and dataset.