ABSTRACT:

Automated theorem proving (ATP) is a well-established field of mathematics and computer science, concerned with how computers can autonomously construct formal proofs. The recent push in the mathematical community towards machine-checkable proofs, together with the rapid progress in Large Language Models (LLMs), has revived it as a frontier research topic.

LLMs have emerged as natural candidates for ATP, already achieving impressive results on several tasks. Yet, LLM-based provers remain unreliable and resource-intensive, in contrast with the structural reliability of symbolic methods, which conversely apply only to a limited set of instances. Current research seeks to combine these approaches, merging generative and symbolic AI.

Building on this, we plan to investigate new agentic paradigms in ATP that allow models to receive direct feedback from proof checkers, lemma-search engines and other external tools, to enhance both performance and efficiency. Our preliminary experiments on program verification support the thesis that agentic systems are the most effective and versatile approach for ATP, and there is growing consensus in the research community in this sense.

Applying data science and AI methods, this project proposes a novel modular, model- and language-agnostic framework for agentic theorem proving. The transparency of open-source libraries will provide deeper insights into each stack component, addressing a key issue of current setups based on private tools like Claude Code. The modularity will be designed to allow granular analysis, replacement, extension and upgrading of each component, including the ability to select LLM backends, proof checkers, MCP tools and domain-specific Agent Skills. The design will also support other ATP-related tasks such as autoformalization.

As practical testbeds, we will pursue innovative data-driven applications in formal program verification and high-assurance cryptography. Employing our framework to synthetically generate new program verification datasets from Rust codebases will address a need for harder benchmarks that our experiments have highlighted. By targeting Rust cryptographic software, the same workflow will be applied to formally certify adherence of implementations to their specifications, guaranteeing correctness of crucial protocols and preventing serious security threats. Finally, many open mathematical questions are awaiting proofs or formalizations: we aspire to contribute to these efforts.