Abstract
We present Ax-Prover, a multi-agent system for automated theorem proving inLean that can solve problems across diverse scientific domains and operateeither autonomously or collaboratively with human experts. To achieve this,Ax-Prover approaches scientific problem solving through formal proofgeneration, a process that demands both creative reasoning and strict syntacticrigor. Ax-Prover meets this challenge by equipping Large Language Models(LLMs), which provide knowledge and reasoning, with Lean tools via the ModelContext Protocol (MCP), which ensure formal correctness. To evaluate itsperformance as an autonomous prover, we benchmark our approach against frontierLLMs and specialized prover models on two public math benchmarks and on twoLean benchmarks we introduce in the fields of abstract algebra and quantumtheory. On public datasets, Ax-Prover is competitive with state-of-the-artprovers, while it largely outperform them on the new benchmarks. This showsthat, unlike specialized systems that struggle to generalize, our tool-basedagentic theorem prover approach offers a generalizable methodology for formalverification across diverse scientific domains. Furthermore, we demonstrateAx-Prover's assistant capabilities in a practical use case, showing how itenabled an expert mathematician to formalize the proof of a complexcryptography theorem.