Persistent proof search improves automation in Lean4 theorem prover
Symbolic Search Is Not Exhausted: Persistent Proof-Space Exploration in Lean4
Logic in Computer Science
Summary
The paper presents a system called ViaLean that helps computers prove mathematical statements more effectively. Instead of blindly checking every possibility, it keeps track of previous work and merges similar goals to avoid repeated effort. This approach lets it solve half of a standard set of math problems automatically. The authors show that better organization of proof steps can significantly improve how computers reason mathematically, and their system can also work alongside AI tools to combine verified reasoning with learned guidance.
What this means in practice
- •For formal verification engineers: Integrate persistent proof-space exploration to enhance automated theorem proving efficiency in software and hardware verification tasks.
- •For ai system developers: Develop neural-symbolic reasoning agents that operate over verified intermediate proof structures to improve machine reasoning accuracy.
Authors
Ruoran Xu
Abstract
Formal theorem proving increasingly combines learned semantic guidance with verified symbolic execution. The quality of the symbolic search substrate therefore determines how much useful mathematical structure can be accumulated, reused, and exposed under a finite inference budget. We introduce ViaLean, a Lean4 prover that organizes symbolic reasoning as bounded exploration of a persistent proof-state graph. Its search preserves coverage across complementary reasoning modes, merges semantically equivalent goals, retains verified intermediate structure, and observes short symbolic futures before committing to a transition. On the complete miniF2F test split, the model-free configuration solves 122/244 problems (50.0% pass@1). Historical and recent symbolic reference points range from Lean's earlier tidy search to modern grind and SMT-backed verification, showing that proof-space organization remains a substantial source of capability. The same persistent state also provides a natural interface for neural--symbolic agents: neural reasoning can operate over verified regions and intermediate objects while Lean continuously expands and validates the local proof space.