| title | Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search |
|---|---|
| authors | Jialin Lu, Soonho Kong, Rodrigo Stehling, Kaiyu Yang, Zhangyang Wang, Weiran Sun, Wuyang Chen |
| date | 2026-05-18 |
| venue | arXiv (preprint, not peer reviewed) |
| id | arXiv:2605.20244 |
| upvotes | 2 (Hugging Face Daily Papers, 2026-11-01) |
| links | abs pdf hf |
| abstract | 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. |
cite
@misc{lu2026lean,
title={Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search},
author={Jialin Lu and Soonho Kong and Rodrigo Stehling and Kaiyu Yang and Zhangyang Wang and Weiran Sun and Wuyang Chen},
year={2026},
eprint={2605.20244},
archivePrefix={arXiv},
url={https://arxiv.org/abs/2605.20244}
}