We present Lean Refactor, a plug-and-play retrieval-augmented agentic framework for multi-objective, controllable, and version-robust refactoring of Lean proofs. LLM-generated proofs are notoriously correct-but-verbose and brittle across library versions, yet existing refactoring works overlook three practical challenges: 1) Lean refactoring is natively multi-objective (proof length, compilation cost, and version compatibility are often in tension); 2) Lean repositories have fragile compatibility, whereas LLM releases are unaware of Lean/Mathlib versions; 3) Training-based pipelines require repeated fine-tuning with each new LLM release, scaling neither with model churn nor with Lean's release cycle. Lean Refactor steers a frozen agentic LLM with retrievals from a curated database of multi-objective refactoring strategies, each densely annotated with metadata such as supported Lean/Mathlib versions and expected compilation-cost reduction. Experiments show over $70\%$ token-level compression on competition benchmarks, over $20\%$ on research repositories, and up to $60\%$ compilation-time reduction, outperforming prior work and Claude Code. Version-filtered retrieval further improves compression on the target Lean version, and refactored miniF2F proofs exhibit stronger zero-shot version transfer to future Lean releases than their unrefactored counterparts.

翻译：我们提出Lean Refactor，一种即插即用的检索增强智能体框架，用于对Lean证明进行多目标、可控且版本鲁棒的优化。LLM生成的证明以其准确但冗长且跨库版本脆弱而著称，然而现有优化工作忽视了三个实际挑战：1) Lean证明优化本质上是多目标的（证明长度、编译代价与版本兼容性之间通常存在权衡）；2) Lean仓库具有脆弱兼容性，而LLM发布版本对Lean/Mathlib版本信息不敏感；3) 基于训练的方法需要随每个新LLM版本发布反复微调，既无法随模型迭代扩展，也无法适应Lean的发布周期。Lean Refactor通过从包含多目标优化策略的精选数据库中检索信息来引导冻结的智能体LLM，每条策略均带有丰富的元数据注释（如支持的Lean/Mathlib版本及预期的编译代价缩减量）。实验表明，该方法在竞赛基准上实现超过70%的词元级压缩，在研究仓库上实现超过20%的压缩，并实现高达60%的编译时间缩减，优于先前工作与Claude Code。基于版本过滤的检索进一步提升了目标Lean版本上的压缩效果，经优化的miniF2F证明在向未来Lean版本的零样本版本迁移中展现出比未优化版本更强的鲁棒性。