The bottleneck no one saw in AI math proofs: decomposition, not compute

Formal mathematical proofs, the kind checked by machines, not humans, are the gold standard of rigor. But translating the informal proofs mathematicians write in natural language into formal languages like Lean remains a stubborn, long-horizon challenge. A team from Nanjing University and Polixir Technologies now says they have cracked a key bottleneck in that pipeline.

Their framework, called ToMap (Test-time Optimization for Multi-Agent Proof autoformalization), treats full-proof formalization not as a single translation task but as a three-stage multi-agent system: a Decomposer that splits the proof into atomic units, a Formalizer that renders each unit in Lean syntax, and a Prover that generates the tactics to close each goal. The surprise finding, published in a preprint, is that the weakest link is the first stage, and that focusing compute on improving just the decomposition yields outsized gains. This mirrors the approach of M3's evolutionary search for math verifiers but applied to a different problem entirely.

The bottleneck analysis

To identify where test-time compute is best spent, the researchers ran a controlled intervention experiment. Under identical Lean error traces and a fixed correction budget, they allowed only one of the three agents to revise its output while freezing the other two. The Decomposer intervention consistently achieved the highest full-proof accuracy: 51.1% after five passes on the 184-sample ProofFlowBench, versus 45.1% for the Formalizer and 33.7% for the Prover.

"The Decomposer sets the difficulty of every downstream obligation," the authors write. A decomposition that produces atomic, self-contained proof units with explicit dependencies reduces formalization and proving to local tasks that the downstream agents can handle. Poorly scoped units leave the executor with ambiguous or incomplete goals.

How ToMap works

Rather than distributing test-time compute across all three agents, ToMap concentrates it on the Decomposer. It maintains a pool of candidate natural-language decompositions, scores each against a three-dimensional rubric (semantic faithfulness, provability, and Lean-friendliness), and uses the resulting Pareto frontier to guide iterative evolution of the decomposition prompts, a technique inspired by the GEPA algorithm for reflective prompt optimization.

A commit gate reserves the expensive downstream Formalizer-Prover-Lean verification cycle for candidates that meet a minimum threshold on all three rubric dimensions. "Rubric feedback is cheap and dense, steering the bulk of the search, while Lean verification provides faithful but expensive ground-truth signals reserved for promising candidates," the authors explain.

Results and comparisons

On ProofFlowBench, ToMap powered by Gemini3-Pro achieved a joint syntactic correctness and semantic faithfulness score of 40.22%, a 19.0 percentage point improvement over the best previous method, Codex End2End (21.20%). On miniF2F, the dataset of high-school-level competition problems, ToMap reached 55.74%, an 8.2% improvement. The system also outperformed training-based approaches like ProofBridge, which requires a retrieval model and a fine-tuned translator, while keeping inference-only costs lower. To put those cost savings in context, Leanstral 1.5 showed similar efficiency gains for formal verification with a far smaller model.

Ablation studies reveal a clear time-performance trade-off: most gains emerge within 3-5 evolution iterations, after which returns diminish. That gives practical guidance for picking the iteration budget under latency or cost constraints.

"Methods that generate a single monolithic Lean proof can achieve relatively high syntactic correctness, but they struggle to faithfully translate the individual steps of natural-language proofs," the authors note. "Step-wise proof formalization better preserves semantic faithfulness by explicitly aligning the formalization process with intermediate proof steps."

Limitations and future work

The evaluation is restricted to benchmark-scale proofs, not long research-level mathematics. The system also assumes input proofs are correct, handling incorrect or incomplete informal proofs remains an open problem. Extending the framework to detect and repair flawed reasoning is flagged as future work. One clue that the systems themselves may struggle to correct such reasoning comes from research on AI coding agents, where counting the actual time saved is far harder than measuring code output.

The Nanjing team's contribution is less a breakthrough in formal reasoning capacity than a demonstration that clever allocation of test-time compute, informed by systematic bottleneck analysis, can extract more value from existing models than simply scaling up monolithic approaches. For the growing community working to bridge informal and formal mathematics, that insight may prove as valuable as the benchmarks themselves.