Title: Proof-Refactor: Transforming Generated Formal Proofs into Modular Components

Abstract:

Although Large Language Models (LLMs) have demonstrated considerable proficiency in producing formal proofs, the resulting scripts typically lack the readability, modularity, maintainability, and reusability characteristic of established formal mathematics libraries. We posit that this deficiency is partly attributable to the "compile-first" mindset embedded in most proof-generation workflows, which tends to produce monolithic or ad hoc scripts rather than high-quality, library-standard artifacts. While current methods for enhancing proof quality often depend on explicit, computable optimization goals, practical applications reveal that the most viable and experimentally supported metrics are primarily focused on length. Conversely, higher-order attributes such as readability and modularity resist reduction to reliable automated metrics. Rather than optimizing for a single proxy measure, we adopt a process-guided strategy modeled after human refactoring practices. We introduce Proof-Refactor, an agentic framework that breaks down the refactoring process into four distinct stages: identifying candidate proof fragments, formulating helper declarations, formally verifying these extracted and designed elements, and reconstructing the original proof using these verified components. Evaluated on generated Lean proofs from the PutnamBench and Putnam2025 datasets, Proof-Refactor outperforms a robust Claude Code refactoring baseline in rubric-based refactoring scores, achieving its most significant improvements in signature quality and human readability. These findings indicate that structuring refactoring through guided processes can enhance proof architecture without prioritizing brevity as the main goal.

Source: arXiv Generated at: 2026-06-03 00:00:00 UTC