TY  - RPRT
TI  - Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
AU  - Jialin Lu
AU  - Soonho Kong
AU  - Rodrigo Stehling
AU  - Kaiyu Yang
AU  - Zhangyang Wang
AU  - Weiran Sun
AU  - Wuyang Chen
PY  - 2026
UR  - https://arxiv.org/abs/2605.20244
ID  - 2605.20244
ER  -