Lean Refactor：基于代理策略搜索的多目标可控证明优化

本文提出 Lean Refactor，一种即插即用的检索增强型代理框架，旨在实现多目标、可控且版本鲁棒的 Lean 证明重构。针对现有方法忽视的多目标冲突、库版本兼容性脆弱及训练流水线扩展性差等挑战，该框架利用 curated 策略数据库引导冻结的代理 LLM。实验表明，其在竞赛基准上实现了超过 70% 的令牌级压缩，编译时间减少高达 60%，显著优于先前工作及 Claude Code，并展现出更强的零样本版本迁移能力。