Ax-Prover: a deep reasoning agentic framework for theorem proving in mathematics and quantum physics

Source abstract

Abstract We present Ax-Prover, a multi-agent system for automated theorem proving in Lean that can solve problems across diverse scientific domains and operate either autonomously or collaboratively with human experts. To achieve this, Ax-Prover approaches scientific problem solving through formal proof generation, a process that demands both creative reasoning and strict syntactic rigor. Ax-Prover meets this challenge by equipping large language models (LLMs), which provide knowledge and reasoning, with custom Lean tools which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against both frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks that we introduce in abstract algebra and quantum theory. On the public datasets, Ax-Prover is the top prover among those that do not rely on any domain-specific training; on the new benchmarks, it largely outperforms all baselines. Together, these results suggest that tool-based agentic theorem proving can support formal verification across benchmarks with different mathematical and scientific structure. Furthermore, we showcase Ax-Prover as a researcher-friendly assistant through two practical case studies in classical and quantum cryptography, pillars of secure communication, where it worked with domain experts to formalize and verify challenging security guarantees using standard human–agent interactions, enabling those without expertise in Lean to engage in this burgeoning domain.