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通过形式化证明生成这一需要创造性推理与严格语法严谨性的过程来处理科学问题求解。该系统通过模型上下文协议（MCP）为具备知识与推理能力的大语言模型（LLMs）配备Lean工具，从而确保形式正确性。为评估其作为自主证明器的性能，我们在两个公开数学基准及两个自建的抽象代数与量子理论领域Lean基准上，将本方法与前沿LLMs及专用证明器模型进行对比测试。在公开数据集上，Ax-Prover与最先进的证明器性能相当，而在新基准测试中则显著优于现有方法。这表明，相较于难以泛化的专用系统，我们基于工具的智能体定理证明方法为跨科学领域的形式化验证提供了可泛化的方法论。此外，我们通过实际用例展示了Ax-Prover的辅助能力：该系统成功协助一位数学家完成了复杂密码学定理证明的形式化工作。