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 Lean tools via the Model Context Protocol (MCP), which ensure formal correctness. To evaluate its performance as an autonomous prover, we benchmark our approach against frontier LLMs and specialized prover models on two public math benchmarks and on two Lean benchmarks we introduce in the fields of abstract algebra and quantum theory. On public datasets, Ax-Prover is competitive with state-of-the-art provers, while it largely outperforms them on the new benchmarks. This shows that, unlike specialized systems that struggle to generalize, our tool-based agentic theorem prover approach offers a generalizable methodology for formal verification across diverse scientific domains. Furthermore, we demonstrate Ax-Prover's assistant capabilities in a practical use case, showing how it enabled an expert mathematician to formalize the proof of a complex cryptography theorem.

翻译：我们提出Ax-Prover，一个面向Lean的自动化定理证明多智能体系统，能够解决跨多个科学领域的问题，既可自主运行，也可与人类专家协作。为实现这一目标，Ax-Prover通过形式化证明生成的方式来处理科学问题，这一过程既需要创造性推理，也要求严格的句法严谨性。Ax-Prover通过模型上下文协议（MCP）为大型语言模型（LLMs）配备Lean工具来应对这一挑战——LLMs提供知识与推理能力，而MCP确保形式化正确性。为评估其作为自主证明器的性能，我们在两个公开数学基准测试以及两个我们新引入的抽象代数与量子理论领域Lean基准测试上，将我们的方法与前沿LLMs及专用证明器模型进行对比。在公开数据集上，Ax-Prover与最先进的证明器表现相当；而在新基准测试上，其性能大幅超越后者。这表明，与难以泛化的专用系统不同，我们基于工具的智能体定理证明方法为跨多个科学领域的形式化验证提供了一种可泛化的方法论。此外，我们通过一个实际用例展示了Ax-Prover的辅助能力，说明它如何帮助一位数学家专家完成一个复杂密码学定理的形式化证明。