LeanRefiner: Agentic Global-to-Local Optimization of Lean Proofs

Modern Lean provers are increasingly able to produce proofs that pass mechanical verification. However, a verified proof may still be lengthy, repetitive, and difficult to read or maintain. We formalize this setting as proof optimization after correctness and propose LeanRefiner, a framework for optimizing verified Lean proofs under hard correctness constraints. Given a verified Lean proof, LeanRefiner aims to shorten and reorganize it while preserving the theorem statement, maintaining Lean verifiability, and avoiding proof holes. To achieve this goal, LeanRefiner employs a verifier-guided agentic system that combines theorem-level global restructuring with pattern-guided local reduction over bounded proof fragments. Experiments on three collections of verified Lean proofs show that LeanRefiner consistently reduces proof length while satisfying strict verifier constraints. Further analysis shows that these gains mainly stem from the staged collaboration between the global restructuring and local reduction agents, rather than from superficial cleanup or any specific backend.