OpenProver: Agentic and Interactive Theorem Proving with Lean 4
2026-07-10 • Artificial Intelligence
Artificial IntelligenceMathematical Software
AI summaryⓘ
The authors introduce OpenProver, an open-source system that uses large language models (LLMs) to help automatically prove math theorems, while verifying the proofs with the Lean 4 formal system. Their system organizes the work into a Planner that breaks down tasks, multiple Workers that handle parts in parallel, and a Verifier that checks proofs. OpenProver also supports interactive use, where a person can guide the proof search. The authors test OpenProver on a benchmark dataset and compare it to a basic method, demonstrating its capabilities and providing code for others to try.
Automated Theorem ProvingLarge Language Models (LLMs)Lean 4Formal VerificationPlanner-Worker-Verifier ArchitectureProofNetInteractive Proof SearchOpen-source SoftwareProof DecompositionAgentic Systems
Authors
Matěj Kripner, Milan Straka
Abstract
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, and decomposes 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 https://github.com/kripner/OpenProver.