A Minimal Agent for Automated Theorem Proving

Paper: 2602.24273 Authors: Borja Requena Pozo, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro, Leopoldo Sarra Categories: cs.AI

The Gap

The automated theorem proving landscape has become cluttered with increasingly complex systems—AlphaProof, DeepSeek-Prover, LEGO-Prover—each introducing novel architectural components that make it nearly impossible to isolate what actually drives performance. When one system outperforms another, is it the model size? The search strategy? The training data? The prompt engineering? We can’t tell, because these systems are monolithic black boxes with dozens of interacting design choices. The field lacks a minimal, transparent baseline that implements only the essential components, allowing researchers to conduct controlled experiments and understand which innovations actually matter.

The Increment

Before: Complex theorem provers with entangled components → impossible to attribute performance gains. After: A minimal agent with three decoupled modules → systematic ablation studies become feasible.

Think of this system as a three-stage assembly line for mathematical proofs. The first station (proof refinement) is where a worker repeatedly examines a partially completed proof, identifies the next gap, and attempts to fill it—this is the iterative core that generates proof steps one at a time based on feedback from the proof assistant. The second station (library search) is the reference desk where the worker looks up relevant theorems and lemmas from a vast catalog—implemented as semantic search over the mathematical library to retrieve useful context. The third station (context management) is the quality control checkpoint that decides what information to keep in the worker’s limited attention span—a filtering mechanism that prevents context overflow while retaining critical proof state. Each station operates independently, making it trivial to swap out components or measure their individual contributions.

The architecture deliberately avoids sophistication. No reinforcement learning, no tree search, no ensemble methods—just an LLM in a loop with access to a search index and a context window manager. Yet this simplicity is the point: by stripping away everything non-essential, the authors create a reference implementation that reveals which complexities in existing systems are load-bearing and which are ornamental.

Key Concepts

Iterative Proof Refinement

Imagine you’re solving a jigsaw puzzle, but you can only see one piece at a time, and after placing each piece, someone tells you whether it fits or not. That’s iterative refinement. In formal mathematics, a proof isn’t written in one shot—it’s constructed step-by-step, where each step must be verified by a proof assistant (like Lean or Coq) before you proceed. If a step fails, you get an error message explaining why, and you try again.

The minimal agent implements this as a simple loop: (1) send the current proof state to the LLM, (2) receive a proposed next tactic, (3) execute it in the proof assistant, (4) if it succeeds, append it to the proof and repeat; if it fails, include the error in the next prompt and ask for a correction. This is fundamentally different from generating an entire proof at once, because the LLM gets real-time feedback about what’s valid. It’s like having a compiler that talks back to you after every line of code, rather than only after you hit “run” on the whole program.

Library Search as Retrieval-Augmented Generation

Formal mathematics has a chicken-and-egg problem: to prove theorem X, you often need to invoke lemma Y, but how do you know lemma Y exists in the library? Human mathematicians spend years internalizing their field’s “standard toolkit,” but LLMs don’t have this—they hallucinate lemma names or miss relevant results.

The solution here is semantic search: embed all theorems in the library into a vector space (using something like sentence transformers), then at each proof step, embed the current goal and retrieve the $k$ nearest neighbors. These retrieved theorems get injected into the LLM’s context as “here are some potentially useful facts.” It’s RAG (retrieval-augmented generation) applied to mathematics. The key insight is that you don’t need a fancy learned retriever—even a simple embedding model gives you enough signal to surface relevant lemmas, dramatically reducing hallucination rates.

Context Management

LLMs have finite context windows, but proofs can be arbitrarily long. After 50 proof steps, you’ve accumulated thousands of tokens of history—previous tactics, error messages, retrieved lemmas—and you’re about to hit the context limit. What do you keep?

The minimal agent uses a sliding window with priority retention: always keep the original theorem statement and the current proof state (these are non-negotiable), then fill the remaining space with recent history and high-relevance retrieved lemmas. Older steps get evicted first, under the assumption that recent context is more predictive of the next step. This is crude but effective—it’s the difference between a system that crashes after 30 steps and one that can handle 200-step proofs. More sophisticated approaches (like compressing history with a summarization model) are possible, but the authors show you can get surprisingly far with this simple heuristic.

Expert Assessment

Problem significance: High. Automated theorem proving is a testbed for AI reasoning capabilities, and the lack of standardized baselines has made progress hard to measure. The affected community includes not just formal verification researchers, but anyone working on AI for mathematics, code synthesis, or multi-step reasoning. This paper provides infrastructure that should accelerate the field.

Method maturity: This is a reference implementation, not a production system. The authors are explicit about limitations—no learning from feedback, no sophisticated search strategies, no handling of proof repair beyond simple retry. The architecture is deployment-ready in the sense that it’s stable and reproducible, but it’s not designed to be the best prover; it’s designed to be the simplest prover that’s still competitive. That’s a feature, not a bug, but it means practitioners looking for state-of-the-art performance will need to add components back in.

Experimental rigor: Strong. The authors test on multiple benchmarks (miniF2F, ProofNet, and others) with different characteristics, compare against both simple baselines (single-shot generation) and complex systems (AlphaProof-style approaches), and ablate each component to show its contribution. One potential concern: the paper doesn’t deeply explore failure modes—when the minimal agent fails, is it because the problem is genuinely hard, or because some missing component (like tree search) would have solved it? More error analysis would strengthen the claims.

Verdict: Weak accept — valuable contribution to research infrastructure, but limited novelty in individual components; the value is in the integration and the open-source release, not in algorithmic innovation.

Takeaways

Simplicity as a research tool: When a field gets too complex, the highest-leverage move is often to build the simplest thing that works, then use it as a baseline to measure everything else. This applies beyond theorem proving—any domain with proliferating architectures (e.g., code generation, robotics planning) would benefit from a “minimal agent” that isolates core components.

Iterative refinement beats one-shot generation: The paper shows consistent gains from letting the model see feedback and retry, even with no learning. This pattern transfers directly to code synthesis (run the code, see the error, fix it), dialogue systems (get user feedback, refine the response), and scientific reasoning (propose hypothesis, see experimental result, update). The key is closing the loop between generation and evaluation.

Retrieval is underrated: Many researchers focus on making models bigger or training them longer, but this paper shows that a simple semantic search over a knowledge base can match or exceed the gains from scale. If your domain has a structured knowledge source (API docs, scientific literature, legal precedents), embedding-based retrieval should be your first move before reaching for a larger model.

Context management is a first-class design problem: As tasks get longer (multi-turn conversations, long-horizon planning, extended proofs), what you keep in context matters as much as the model itself. The sliding window with priority retention is a transferable pattern—always preserve the task specification and current state, then allocate remaining space to recent history and high-relevance retrieved information.