# OpenProver: Agentic and Interactive Theorem Proving with Lean 4

arXiv: https://arxiv.org/abs/2607.09217 · HTML: https://mlsanity.com/paper/2607.09217/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use.
- Builds on 9 of its 13 references that are in the map.
- First posted on arXiv 10 Jul 2026.

## Placed in

- LLM agents and tool use / [Educational agents and math problem solving](https://mlsanity.com/agents/educational-agents-and-math-problem-solving/)

## Builds on (most cited first, 9 of 9)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [AlphaEvolve: A coding agent for scientific and algorithmic discovery](https://mlsanity.com/paper/2506.13131/) (2025)
- [Kimi K2.5: Visual Agentic Intelligence](https://mlsanity.com/paper/2602.02276/) (2026)
- [Reinforcement Learning with Verifiable Rewards Implicitly Incentivizes Correct Reasoning in Base LLMs](https://mlsanity.com/paper/2506.14245/) (2025)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [Feedback Descent: Open-Ended Text Optimization via Pairwise Comparison](https://mlsanity.com/paper/2511.07919/) (2025)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [Reasoning Cache: Continual Improvement Over Long Horizons via Short-Horizon RL](https://mlsanity.com/paper/2602.03773/) (2026)

## Built on by (most cited first, 2 of 2)

- [VALG: An Agentic System for ML Theory Research](https://mlsanity.com/paper/2608.13060/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)

## Abstract (arXiv)

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.