Keep the Proof State Live: Snapshotting for Efficient Tactic Search in Lean 4

Researchers introduce proof-state snapshotting, a technique that accelerates automated theorem proving in Lean 4 by reusing elaborated proof states across parallel search branches instead of reconstructing them. The method achieves 5.6-50x speedups (averaging 14x) on benchmark problems, addressing a critical bottleneck where per-branch overhead from import loading and elaboration consumed over 99% of computation time.

Automated theorem proving represents a critical frontier in AI-assisted mathematics and formal verification, enabling systems to verify complex mathematical proofs with machine assistance. The Lean 4 ecosystem has become central to this effort, particularly through pipelines like Draft-Sketch-Prove that generate partially specified proofs requiring parallel search to complete. However, the current execution model creates severe inefficiencies: each search branch independently reconstructs the entire proof state by re-running library imports and re-elaborating theorem contexts, resulting in redundant computation measured in hundreds of seconds per branch.

This bottleneck stems from an architectural mismatch between how proof search is conceptualized—as branching exploration—and how it executes—as serialized state reconstruction. The snapshotting approach directly addresses this by capturing the elaborated state once and reusing it across branches, requiring only minimal modifications to Lean 4's language server infrastructure. The empirical results demonstrate substantial practical impact: speedups scale with branching factor and reach 50x on complex problems.

For the theorem proving and formal verification communities, this optimization unlocks portfolio-based search strategies previously impractical due to computational costs. Developers building AI-assisted proof systems can now explore wider search spaces within reasonable time budgets. The orthogonal nature of this approach—complementing rather than replacing import-level caching—suggests multiplicative efficiency gains when combined with other optimizations. The commitment to open-source release amplifies industry impact by democratizing access to these techniques across academic and commercial research groups working on automated mathematics and formal methods.

• →Proof-state snapshotting reduces per-branch overhead from >99% to minimal levels, enabling practical parallel tactic search in Lean 4
• →Speedups average 14x and reach 50x on complex benchmarks, scaling with the number of proof search branches
• →The technique is orthogonal to import-level caching, suggesting potential for further optimization when combined with complementary approaches
• →Open-source release of the patched Lean binary and Snapshot-DSP pipeline will accelerate adoption across theorem proving research
• →This work removes a critical bottleneck in automated mathematics, enabling AI systems to explore wider proof spaces efficiently