A Minimal Agent for Automated Theorem Proving

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.

Mathematical proofs are essential for verifying results in mathematics, science, and engineering, but writing these proofs is difficult and time-consuming. We build a simple AI-based theorem prover that writes these proofs using a programming language that enables them to be automatically checked by a computer. The system is designed to be accessible, cost-effective, broadly-applicable, and to naturally improve as generative AI models become stronger without requiring any further significant modification. We show that a simple system can achieve competitive performance with much more complex ones while operating at a fraction of their cost. We release it openly for the community to use as a tool in their own projects, as well as starting point for researchers to develop future theorem-proving systems. This work can make rigorous verification more practical for mathematics, with deep implications in scientific research and engineering. More broadly, it may help move AI toward verified scientific reasoning: systems that generate ideas and explanations together with machine-checkable evidence for their correctness.