A Minimal Agent for Automated Theorem Proving

TL;DR

This paper introduces a simple, open-source agentic framework for automated theorem proving that achieves competitive results with less complexity and cost than existing systems.

Contribution

It presents a minimal, modular agentic architecture for theorem proving, enabling systematic comparison and demonstrating advantages of iterative proof refinement.

Findings

Competitive performance with simpler architecture

Iterative approach outperforms single-shot methods

Cost-effective and sample-efficient proof generation

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 this agentic approach using qualitatively different benchmarks and compare various frontier language models and design choices. Our results show competitive performance compared to state-of-the-art approaches, while using a significantly simpler architecture and a fraction of their cost. Additionally, we 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.