LeanPolish：面向 Lean 形式化证明压缩的已验证监督框架

研究人员推出 Lean 4 形式化证明压缩符号管道 LeanPolish，并公开了 33,402 条验证通过的局部编辑及 65,596 条失败尝试数据。基于该监督训练的排序器在测试集状态下选择最佳候选的准确率达 70.1%，远超冻结基线的 36.9%，且迭代符号处理将 miniF2F 压缩率提升至 27.5%。