A Minimal Agent for Automated Theorem Proving
2026-02-27 • Artificial Intelligence
Artificial Intelligence
AI summaryⓘ
The authors created a simple, basic AI system for proving math theorems that includes key features seen in advanced systems, like improving proofs step-by-step and searching helpful libraries. They tested it on different challenges and found it works well compared to more complex systems. Their approach of refining proofs repeatedly is more efficient and cheaper than trying to get the answer in one go. They shared their code publicly so others can use and build on it.
AI theorem provingiterative refinementlibrary searchcontext managementsample efficiencyproof generationmachine learning modelsopen-source software
Authors
Borja Requena Pozo, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro, Leopoldo Sarra
Abstract
We propose a minimal agentic baseline that enables systematic comparison across different AI-based theorem prover architectures. This design implements the core features shared among state-of-the-art systems: iterative proof refinement, library search and context management. We evaluate our baseline using qualitatively different benchmarks and compare various popular models and design choices, and demonstrate competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture. Our results demonstrate consistent advantages of an iterative approach over multiple single-shot generations, especially in terms of sample efficiency and cost effectiveness. The implementation is released open-source as a candidate reference for future research and as an accessible prover for the community.