LeanPolish：面向 Lean 证明压缩的形式验证监督

LeanPolish 推出面向 Lean 4 证明压缩的符号化流水线，并发布 33,402 条验证通过的局部编辑与 65,596 条失败尝试数据。基于该数据训练的排序器在 70.1% 的保留状态中选出最佳候选，优于冻结基准的 36.9%。