OpenProver: Agentic and Interactive Theorem Proving with Lean 4

# Agentic and Interactive Theorem Proving with Lean 4
Source: [https://arxiv.org/html/2607.09217](https://arxiv.org/html/2607.09217)
11institutetext:Charles University, Faculty of Mathematics and Physics, Prague, Czech Republic
11email:\{kripner,straka\}@ufal\.mff\.cuni\.cz###### 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[github\.com/kripner/OpenProver](https://github.com/kripner/OpenProver)\.

## 1Introduction

Automated Theorem Proving \(ATP\) has seen a significant rise in capabilities with the integration of Large Language Models \(LLMs\) trained using Reinforcement Learning from Verifiable Rewards \(RLVR\)\[[13](https://arxiv.org/html/2607.09217#bib.bib13)\]\. Beyond tackling some of the hardest problems in competition mathematics, we are now seeing sparks of usefulness of ATP systems in frontier mathematical research\.

Existing ATP systems can be roughly divided into two categories\. First, fully autonomous theorem provers attempt end\-to\-end proof generation without human intervention, enabling reproducibility across runs\. An example of such a system is Aletheia\[[3](https://arxiv.org/html/2607.09217#bib.bib3)\]\.

Second, interactive theorem provers \(ITPs\) enable the user to monitor and intervene in the proof search process, following the observation that while autonomous AI systems do not yet match expert human performance, the integration of both can greatly accelerate research\. For example, a mathematician can formulate several potential approaches to completing a certain proof, receive worked\-out counterexamples and observations from an AI assistant, and use these to iteratively adjust the high\-level plan\. With a human operator in the loop, ITP approaches require careful design of the visual user interface\. Concurrent to our work, several agentic LLM\-based ITP tools have been released, including OpenGauss\[[6](https://arxiv.org/html/2607.09217#bib.bib6)\]\.

We present OpenProver, an automated theorem prover that bridges the gap between reproducible ATP research and interactive mathematical tooling\. OpenProver extends Aletheia, most notably by integrating formal verification capabilities of Lean 4\[[8](https://arxiv.org/html/2607.09217#bib.bib8)\]\. To showcase the automatic evaluation enabled by Lean, we present quantitative measurements of OpenProver performance on ProofNet\[[2](https://arxiv.org/html/2607.09217#bib.bib2)\], compared to a simple linear Chain\-of\-Thought baseline\. We hope that our work advances progress towards ATP systems that are both useful in frontier mathematical research and whose performance can be rigorously measured\.

## 2System Description

![Refer to caption](https://arxiv.org/html/2607.09217v1/x1.png)Figure 1:Overview of the OpenProver proof search loop\. Planner iterates on the high\-level plan, manages persistent state, and delegates mathematical work to Workers\. A Verifier provides independent feedback to each Worker contribution\.OpenProver is an automated theorem prover utilizing a reasoning LLM executed in an agentic scaffolding, with integration of the Lean 4 formal verifier\. The system operates in an iterative loop composed of three types of agents illustrated in Figure[1](https://arxiv.org/html/2607.09217#S2.F1): a singlePlanner, parallelWorkers, and parallelVerifiers\.

### 2\.1Architecture

During proof search, OpenProver utilizes three distinct types of agents:

1. 1\.Planner:Maintains global state and determines a high\-level plan\.
2. 2\.Workers:Independently explore candidate proof strategies, lemmas, counterexamples, and similar\.
3. 3\.Verifiers:Independently verify each Worker output, providing additional context to the Planner\.

The proof search process is structured as a sequence of Planner steps, described in more detail in Section[2\.3](https://arxiv.org/html/2607.09217#S2.SS3)\.

#### 2\.1\.1Planner

At each step, the Planner first generates a chain\-of\-thought reasoning trace\[[12](https://arxiv.org/html/2607.09217#bib.bib12)\]before producing an output and a list of actions\. The available Planner actions are listed in Table[1](https://arxiv.org/html/2607.09217#S2.T1)and explained in more detail in the following\.

Table 1:Planner actions\. One or more actions are executed in each Planner step\.∗Not available in isolation mode\.

#### 2\.1\.2Workers

Workers are independent agents spawned by the Planner\. For each spawned Worker, the Planner provides a plaintext task description that solely specifies the Worker’s purpose\. Example tasks include advancing a specific proof direction, proposing a decomposition of a theorem into sub\-goals, proving a lemma, exploring minimal cases, searching for counterexamples, or proving a simplified version of the theorem\. Additionally, Workers can be tasked with formalizing an existing natural language proof in Lean\.

Importantly, a Worker does not observe the reasoning traces or outputs of previous Workers or of the Planner\. This facilitates independent exploration of distinct proof attempts, where each Worker is not swayed by irrelevant context\.

#### 2\.1\.3Verifiers

For each finished Worker, we spawn a Verifier tasked with producing an independent natural language feedback with the goal of revealing flaws in the Worker output\. Crucially, the Verifier does not observe the Worker’s reasoning trace, reducing bias toward following the same, potentially flawed, line of thinking\.

### 2\.2State and Memory Management

To preserve important context between Planner steps, OpenProver manages a single compact Markdown file called theWhiteboard, updated periodically by the Planner using thewrite\_whiteboardaction\. While the content of the Whiteboard is decided solely by the Planner, it is advised by the corresponding prompt to contain at least the currently executed proof plan, the history of all already explored and failed attempts, and ideas to return to later, together with any useful brief observations and notes\. The Whiteboard is provided to the Planner as input at each step\. This design can be seen as analogous to the Reasoning Cache\[[14](https://arxiv.org/html/2607.09217#bib.bib14)\], extending the effective context length of reasoning LLMs\.

Additionally, the Planner occasionally needs to store longer text or Lean snippets such as detailed failed proof attempts, proofs of lemmas, literature summaries, and similar\. To prevent overflowing the Whiteboard, OpenProver manages aRepositoryof items where eachItemis either a Markdown file or a Lean file\. Items are organized in a folder\-like structure using thewrite\_itemsandread\_itemsactions, and are referred to by their relative path, which we call aslug\. At each Planner step, alongside the Whiteboard, the Planner also observes the slugs and one\-line summaries of all Items stored in the Repository\. Crucially, Lean Items are only stored if they pass the Lean formal verification; otherwise, the errors and warnings are fed back to the Planner\. This enables tighter feedback from the formal verifier than just a final\-answer check\.

### 2\.3Proof Search Loop

OpenProver executes a linear proof search loop outlined in Algorithm[2](https://arxiv.org/html/2607.09217#S2.F2)until either a proof is found or the compute budget runs out\. Parallelization is enabled by spawning multiple Workers\.

Input:theorem\.md; optionallytheorem\.lean; token budget

BB
Output:proof\.md,discussion\.md; optionallyproof\.lean

1

2Initialize Whiteboard

W←∅W\\leftarrow\\emptyset, repo

R←∅R\\leftarrow\\emptyset, history

H←\[\]H\\leftarrow\[\];

3while*budget not exhaustedandproof\.mdnot yet produced*do

4PlannerStep\(

W,R,HW,R,H\);

5

6\(optionally, iteratePlannerStepfurther untilproof\.leanis produced\);

7writediscussion\.mdsummarizing proof search process and result;

Algorithm 1OpenProver: high\-level operation
In/Out :Whiteboard

WW, repo summary

R′R^\{\\prime\}, history

HH, theorem

TT
1Query planner LLM with

\(W,R′,H−n:,T\)\(W,\\ R^\{\\prime\},\\ H\_\{\-n:\},T\):;

2Produce reasoning trace \(CoT\);

3Produce free\-form output and a list of actions

a1,…,aka\_\{1\},\\dots,a\_\{k\};

4Run

a1,…,aka\_\{1\},\\dots,a\_\{k\}in parallel and wait for completion;

5Append each action’s output to

HH;

Algorithm 2PlannerStep

Figure 2:High\-level pseudocode of OpenProver: the main loop \(Alg\. 1\) repeatedly invokesPlannerStep\(Alg\. 2\)\.
### 2\.4Integration with Lean

OpenProver optionally integrates with the Lean formal verifier, with the only requirement that the formal theorem statement is provided on input in the form of a Lean file with one or moresorrykeywords\.

First, after a natural language proof is found, OpenProver attempts to formalize it and submit the resulting Lean proof\. In case of errors or warnings emitted by the Lean verifier, OpenProver iteratively attempts to fix the proof, potentially transitioning back to fixing the natural language proof in case a flaw is identified\.

Second, the Planner can verify the correctness of any intermediate result by storing it as a Lean Item in the Repository\. Third, Workers can execute Lean\-relatedTool Calls\[[10](https://arxiv.org/html/2607.09217#bib.bib10)\]with the following three tools available:

- •lean\_verify– Verify the correctness of a Lean snippet\.
- •lean\_search– Perform semantic search over Mathlib\[[11](https://arxiv.org/html/2607.09217#bib.bib11)\]using LeanExplore\[[1](https://arxiv.org/html/2607.09217#bib.bib1)\], obtaining thekkmost relevant definitions\.
- •lean\_store– Append a Lean snippet to a temporary file which is then prepended to each followinglean\_verifyinput\. Typically, this includes imports, namespace openings, definitions, and already proven sub\-lemmas\.

An essential limitation of formal ATP is the fact that formalization is often more challenging than the informal proof search\. This gap is expected to reduce as the Lean ecosystem of already proven building blocks evolves over time\.

## 3Interactive User Interface

OpenProver offers an interactive Terminal User Interface \(TUI\) where the user can monitor and steer the search process\. Specifically, users can:

- •Monitor the streaming output of all agents\.
- •Browse the history of previous Planner steps, inspecting their reasoning trace, action inputs, action outputs, and Whiteboard state\.
- •Interrupt any Worker if its reasoning direction seems unpromising\.
- •Interrupt the Planner and provide textual feedback to steer it\.
- •In Manual mode, the user is prompted to accept each set of Planner actions before they are executed\. When they are rejected, potentially with text feedback, the Planner adjusts before proposing new actions\. This is skipped in Autonomous mode\.

## 4Experiments

Table 2:Performance of OpenProver versus a baseline on ProofNet across models\.We measure OpenProver performance in autonomous mode on 185 formal theorems of ProofNet across different underlying models — Kimi K2\.5\[[4](https://arxiv.org/html/2607.09217#bib.bib4)\]and Leanstral\[[7](https://arxiv.org/html/2607.09217#bib.bib7)\]— and a 100k\-tokens per\-problem budget\. Note that OpenProver is model\-agnostic and can utilize any reasoning model as a building block in agentic proof search\. As a baseline, we unroll each model in a linear conversation under the same token budget, where the model can perform an unlimited number of Lean verifications\. The results of this setup are summarized in Table[2](https://arxiv.org/html/2607.09217#S4.T2)\.

## 5Conclusion

With the presentation of OpenProver, we hope to pave the way towards reproducible research in the field of agentic theorem proving through quantitative evaluations enabled by automatic formal verification\. Additionally, it is conceivable that this automatic evaluation feedback could be used as a guiding signal for an autonomous self\-improvement process in the space of code or LLM prompts, akin to e\.g\. Feedback Descent\[[5](https://arxiv.org/html/2607.09217#bib.bib5)\]or AlphaEvolve\[[9](https://arxiv.org/html/2607.09217#bib.bib9)\]\. At a high level, OpenProver adopts a flexible design that shifts many of the behavior decisions from code to prompts, making pure prompt\-based self\-improvement viable\.

\{credits\}

#### 5\.0\.1Acknowledgements

This project was supported by the grant no\. 25\-18031S of the Czech Science Foundation \(GAČR\), by the Charles University Grant Agency \(GAUK\), project no\. 458326, and by the CEDMO 2\.0 NPO project\. This research was partially supported by SVV project number 260 821\. We acknowledge VSB – Technical University of Ostrava, IT4Innovations National Supercomputing Center, Czech Republic, for awarding this project access to the LUMI supercomputer, owned by the EuroHPC Joint Undertaking, hosted by CSC \(Finland\) and the LUMI consortium through the Ministry of Education, Youth and Sports of the Czech Republic through the e\-INFRA CZ \(grant ID: 90254\)\.

#### 5\.0\.2\\discintname

The authors have no competing interests to declare that are relevant to the content of this article\.

## References

- \[1\]Asher, J\.: LeanExplore: A search engine for Lean 4 declarations \(2025\),[https://arxiv\.org/abs/2506\.11085](https://arxiv.org/abs/2506.11085)
- \[2\]Azerbayev, Z\., Piotrowski, B\., Schoelkopf, H\., Ayers, E\.W\., Radev, D\., Avigad, J\.: ProofNet: Autoformalizing and Formally Proving Undergraduate\-Level Mathematics \(2023\),[https://arxiv\.org/abs/2302\.12433](https://arxiv.org/abs/2302.12433)
- \[3\]Feng, T\., Trinh, T\.H\., Bingham, G\., Hwang, D\., Chervonyi, Y\., Jung, J\., Lee, J\., Pagano, C\., hyun Kim, S\., Pasqualotto, F\., Gukov, S\., Lee, J\.N\., Kim, J\., Hou, K\., Ghiasi, G\., Tay, Y\., Li, Y\., Kuang, C\., Liu, Y\., Lin, H\., Liu, E\.Z\., Nayakanti, N\., Yang, X\., Cheng, H\.T\., Hassabis, D\., Kavukcuoglu, K\., Le, Q\.V\., Luong, T\.: Towards autonomous mathematics research \(2026\),[https://arxiv\.org/abs/2602\.10177](https://arxiv.org/abs/2602.10177)
- \[4\]Kimi Team: Kimi K2\.5: Visual Agentic Intelligence \(2026\),[https://arxiv\.org/abs/2602\.02276](https://arxiv.org/abs/2602.02276)
- \[5\]Lee, Y\., Boen, J\., Finn, C\.: Feedback Descent: Open\-Ended Text Optimization via Pairwise Comparison \(2025\),[https://arxiv\.org/abs/2511\.07919](https://arxiv.org/abs/2511.07919)
- \[6\]Math Inc\.: OpenGauss: LLM\-based Interactive Theorem Proving System\.[https://github\.com/math\-inc/OpenGauss](https://github.com/math-inc/OpenGauss)\(2026\), gitHub repository
- \[7\]Mistral AI: Leanstral: Open\-Source Foundation for Trustworthy Vibe\-Coding \(2026\),[https://mistral\.ai/news/leanstral](https://mistral.ai/news/leanstral)
- \[8\]Moura, L\.d\., Ullrich, S\.: The Lean 4 theorem prover and programming language\. In: International Conference on Automated Deduction\. pp\. 625–635\. Springer \(2021\)
- \[9\]Novikov, A\., Vũ, N\., Eisenberger, M\., Dupont, E\., Huang, P\.S\., Wagner, A\.Z\., Shirobokov, S\., Kozlovskii, B\., Ruiz, F\.J\.R\., Mehrabian, A\., Kumar, M\.P\., See, A\., Chaudhuri, S\., Holland, G\., Davies, A\., Nowozin, S\., Kohli, P\., Balog, M\.: AlphaEvolve: A coding agent for scientific and algorithmic discovery \(2025\),[https://arxiv\.org/abs/2506\.13131](https://arxiv.org/abs/2506.13131)
- \[10\]Schick, T\., Dwivedi\-Yu, J\., Dessì, R\., Raileanu, R\., Lomeli, M\., Hambro, E\., Zettlemoyer, L\., Cancedda, N\., Scialom, T\.: Toolformer: Language models can teach themselves to use tools\. Advances in neural information processing systems36, 68539–68551 \(2023\)
- \[11\]The Mathlib Community: The Lean mathematical library\. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs\. p\. 367–381\. CPP 2020, Association for Computing Machinery, New York, NY, USA \(2020\)\. https://doi\.org/10\.1145/3372885\.3373824,[https://doi\.org/10\.1145/3372885\.3373824](https://doi.org/10.1145/3372885.3373824)
- \[12\]Wei, J\., Wang, X\., Schuurmans, D\., Bosma, M\., Ichter, B\., Xia, F\., Chi, E\., Le, Q\., Zhou, D\.: Chain\-of\-Thought Prompting Elicits Reasoning in Large Language Models \(2023\),[https://arxiv\.org/abs/2201\.11903](https://arxiv.org/abs/2201.11903)
- \[13\]Wen, X\., Liu, Z\., Zheng, S\., Ye, S\., Wu, Z\., Wang, Y\., Xu, Z\., Liang, X\., Li, J\., Miao, Z\., et al\.: Reinforcement learning with verifiable rewards implicitly incentivizes correct reasoning in base LLMs\. arXiv preprint arXiv:2506\.14245 \(2025\)
- \[14\]Wu, I\., Qu, Y\., Setlur, A\., Kumar, A\.: Reasoning Cache: Continual Improvement Over Long Horizons via Short\-Horizon RL \(2026\),[https://arxiv\.org/abs/2602\.03773](https://arxiv.org/abs/2602.03773)