-14 7 = Introduction

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) [1]. 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 [2].

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 [3].

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 [4]. To showcase the automatic evaluation enabled by Lean, we present quantitative measurements of OpenProver performance on ProofNet [5], 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.

-14 7 = System Description

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: a single Planner, parallel Workers, and parallel Verifiers.

-12 5 = Architecture

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

1. Planner: Maintains global state and determines a high-level plan.

2. Workers: Independently explore candidate proof strategies, lemmas, counterexamples, and similar.

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 [sec:sec:proof95search95loop].

-10 0.4em Planner At each step, the Planner first generates a chain-of-thought reasoning trace [6] before producing an output and a list of actions. The available Planner actions are listed in Table 1 and explained in more detail in the following.

-10 0.4em Workers 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.

-10 0.4em Verifiers 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.

-12 5 = State and Memory Management

To preserve important context between Planner steps, OpenProver manages a single compact Markdown file called the Whiteboard, updated periodically by the Planner using the write_whiteboard action. 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 [7], 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 a Repository of items where each Item is either a Markdown file or a Lean file. Items are organized in a folder-like structure using the write_items and read_items actions, and are referred to by their relative path, which we call a slug. 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.

-12 5 = Proof Search Loop

OpenProver executes a linear proof search loop outlined in Algorithm 2 until either a proof is found or the compute budget runs out. Parallelization is enabled by spawning multiple Workers.

-12 5 = Integration 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 more sorry keywords.

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-related Tool Calls [8] with the following three tools available:

• lean_verify – Verify the correctness of a Lean snippet.

• lean_search – Perform semantic search over Mathlib [9] using LeanExplore [10], obtaining the \(k\) most relevant definitions.

• lean_store – Append a Lean snippet to a temporary file which is then prepended to each following lean_verify input. 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.

-14 7 = Interactive 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.

-14 7 = Experiments

We measure OpenProver performance in autonomous mode on 185 formal theorems of ProofNet across different underlying models — Kimi K2.5 [11] and Leanstral [12] — 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.

-14 7 = Conclusion

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 [13] or AlphaEvolve [14]. 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.

References↩︎