Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

Generated formal proofs often compile but remain hard to read, maintain, and reuse. We study the post-generation refactoring problem: given a verified proof, produce a better-structured verified proof artifact for the same theorem. We introduce $\textbf{Proof-Refactor}$, an agentic framework that decomposes this task into extracting candidate proof fragments, designing helper declarations, proving the extracted and designed components, and repairing the original proof using the verified helpers. The system combines Claude Code, lean-lsp-mcp, a custom lean_extract tool, and independent-context external assistance for fragment selection and helper design. On generated Lean proofs from PutnamBench and Putnam2025, Proof-Refactor improves LLM-as-a-judge rubric-based refactoring scores over a baseline that uses Claude Code with lean-lsp-mcp and lean4-skills, with the largest gains in signature quality and human readability. These results suggest that process-guided refactoring can improve the structure of verified proof artifacts without optimizing directly for proof length.