证明优化

Lean Refactor：基于智能体策略搜索的多目标可控证明优化框架

First-Principle 转发 HuggingFace Daily Papers 2026年5月22日论文，介绍 Lean Refactor 框架。这是一个检索增强智能体系统，用于对 Lean 语言数学证明进行多目标、可控且版本鲁棒的重构。据论文称，该框架在竞赛基准上实现超过 70% 的标记级压缩，研究仓库压缩率超过 20%，编译时间降低高达 60%，并展现出更强的零样本版本迁移能力。