A Minimal Agent for Automated Theorem Proving

Borja Requena, Austin Letson, Krystian Nowakowski, Izan Beltran Ferreiro, Leopoldo Sarra
Proceedings of the 43rd International Conference on Machine Learning, PMLR 306:104861-104905, 2026.

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v306-requena26a, title = {A Minimal Agent for Automated Theorem Proving}, author = {Requena, Borja and Letson, Austin and Nowakowski, Krystian and Ferreiro, Izan Beltran and Sarra, Leopoldo}, booktitle = {Proceedings of the 43rd International Conference on Machine Learning}, pages = {104861--104905}, year = {2026}, editor = {Zhang, Tong and Dudik, Miroslav and Jaggi, Martin and Agarwal, Alekh and Li, Sharon and Schuurmans, Dale and Zhu, Jerry and Berkenkamp, Felix and Dong, Hanze and Bietti, Alberto}, volume = {306}, series = {Proceedings of Machine Learning Research}, month = {06--11 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v306/main/assets/requena26a/requena26a.pdf}, url = {https://proceedings.mlr.press/v306/requena26a.html}, 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.} }
Endnote
%0 Conference Paper %T A Minimal Agent for Automated Theorem Proving %A Borja Requena %A Austin Letson %A Krystian Nowakowski %A Izan Beltran Ferreiro %A Leopoldo Sarra %B Proceedings of the 43rd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2026 %E Tong Zhang %E Miroslav Dudik %E Martin Jaggi %E Alekh Agarwal %E Sharon Li %E Dale Schuurmans %E Jerry Zhu %E Felix Berkenkamp %E Hanze Dong %E Alberto Bietti %F pmlr-v306-requena26a %I PMLR %P 104861--104905 %U https://proceedings.mlr.press/v306/requena26a.html %V 306 %X 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.
APA
Requena, B., Letson, A., Nowakowski, K., Ferreiro, I.B. & Sarra, L.. (2026). A Minimal Agent for Automated Theorem Proving. Proceedings of the 43rd International Conference on Machine Learning, in Proceedings of Machine Learning Research 306:104861-104905 Available from https://proceedings.mlr.press/v306/requena26a.html.

Related Material