Self-Evolving Decomposition for Multi-Agent Proof Autoformalization

Large language models are beginning to produce proofs at the frontier of mathematics, whose correctness can no longer rest on human review alone. Formal verification in Lean has thus become the standard for certifying such results, and autoformalization is the bridge from informal proofs to verifiable ones. Existing efforts mostly formalize only the theorem statement. However, verifying the reasoning requires formalizing the entire proof, which is crucial for frontier mathematics yet remains underexplored. Current approaches either train models at high cost or retry blindly at inference time. We introduce ToMap, a pipeline of a Decomposer, a Formalizer, and a Prover that evolves at test time under the guidance of rubrics and Lean verification. Bottleneck analysis identifies the Decomposer as the critical stage, since its proof units govern whether downstream agents succeed. ToMap therefore keeps the Formalizer and the Prover fixed and spends its test time computing on the decomposition alone. At its core, ToMap maintains a pool of candidate decompositions, scores each one with rubrics, and evolves those on the Pareto frontier. A frontier candidate whose rubric scores all exceed a threshold is then verified in Lean. If it fails, its diagnostics guide the next round. The decomposition thus self-evolves at test time. On ProofFlowBench and miniF2F, ToMap improves verified and faithful formalization by an average of 20.3% in absolute terms over the strongest training-free baseline, with less running time, and most of the improvement arrives within the first few iterations.