{"ID":6497762,"CreatedAt":"2026-07-13T01:19:40.13847098Z","UpdatedAt":"2026-07-14T01:36:59.12045529Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.09217","arxiv_id":"2607.09217","title":"OpenProver: Agentic and Interactive Theorem Proving with Lean 4","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.","short_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 Whiteboa...","url_abs":"https://arxiv.org/abs/2607.09217","url_pdf":"https://arxiv.org/pdf/2607.09217v1","authors":"[\"Matěj Kripner\",\"Milan Straka\"]","published":"2026-07-10T09:07:12Z","proceeding":"cs.AI","tasks":"[\"cs.AI\",\"cs.MS\"]","methods":"[\"Large Language Model\"]","has_code":false,"code_links":[{"ID":614108,"CreatedAt":"2026-07-13T01:19:40.13847098Z","UpdatedAt":"2026-07-13T01:19:40.13847098Z","DeletedAt":null,"paper_id":6497762,"paper_url":"https://arxiv.org/abs/2607.09217","paper_title":"OpenProver: Agentic and Interactive Theorem Proving with Lean 4","repo_url":"https://github.com/kripner/OpenProver","is_official":false,"mentioned_in_paper":false,"mentioned_in_github":true,"github_stars":0}]}