Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search. - Jialin Lu; Soonho Kong; Rodrigo Stehling; Kaiyu Yang; Zhangyang Wang; Weiran Sun; Wuyang Chen 001 (CoRR, 2026)