In this system paper, we present OpenProver, an open-source system for LLM-driven automated theorem proving (ATP) with integrated Lean 4 formal verification.
OpenProver integrates a Planner-Worker-Verifier architecture inspired by recent ATP agentic systems such as Aletheia.
A Planner agent maintains a compact Whiteboard scratchpad and an unbounded Repository of intermediate findings, decomposing mathematical work into parallel Workers.
OpenProver is fully open-source, offers reproducible evaluation through automatic formal verification of generated proofs, and provides an interactive terminal interface for human-guided proof search.
In interactive mode, OpenProver allows the human operator to monitor and steer the proof search process, motivated by the established human-AI synergy in interactive code generation.
To showcase the potential for quantitative ablation experiments enabled by automatic formal verification, we evaluate OpenProver on ProofNet and compare it with a simple baseline.
OpenProver is publicly available at GitHub.
Blogger's Review: The design of OpenProver showcases the potential of LLMs in theorem proving, providing a powerful tool to enhance human-machine collaboration through integrated Lean 4 formal verification. This novel architecture introduces new concepts to the theorem proving domain, warranting further exploration and development.