FIPO-Prover: Formalization-Oriented Informal Proof Optimization for Efficient Formal Theorem Proving

We presented FIPO-Prover, a verification-guided framework that reformulates informal-to-formal theorem proving as optimization over an evolving Formalization-oriented Informal Proof (FIP) search graph. FIPO-Prover addresses the gap between informal reasoning and formal verification by converting informal proofs into diagnosable, repairable, and projection-friendly intermediate states. Through step-level causal pairs and verifier feedback from Isabelle, the system enables targeted revision, repair, expansion, pruning, upstream backtracking, and memory-guided search. Experiments demonstrate improved formalization reliability and search efficiency over direct generation and prior decomposition-style methods. These results highlight intermediate proof optimization as a promising direction for scalable formal proof search.