Ax-Prover：面向数学与量子物理定理证明的深度推理智能体框架
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
Ax-Prover 是一个基于 Lean 的多智能体自动定理证明系统，通过 MCP 将 LLM 与 Lean 工具结合，兼顾推理能力与形式正确性。在两个公开数学基准上与最先进的证明器相当，并在团队新增的抽象代数与量子理论两个 Lean 基准上大幅超越专用证明模型。该系统还可辅助数学家形式化复杂密码学定理证明，但该论文目前已因未达 arXiv 质量标准被撤回。
This paper has been withdrawn by arXiv Admin
No PDF available, click to view other formats
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 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.
| Comments: | arXiv admin note: This submission has been withdrawn because it does not meet arXiv's research content quality standards |
| Subjects: | Artificial Intelligence (cs.AI); Multiagent Systems (cs.MA) |
| Cite as: | arXiv:2510.12787 [cs.AI] |
| (or arXiv:2510.12787v5 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2510.12787 arXiv-issued DOI via DataCite |
Submission history
From: arXiv Admin [view email]
[v1]
Tue, 14 Oct 2025 17:57:04 UTC (1,937 KB)
[v2]
Thu, 16 Oct 2025 14:10:07 UTC (1,937 KB)
[v3]
Thu, 13 Nov 2025 18:56:10 UTC (1,616 KB)
[v4]
Fri, 22 May 2026 10:39:41 UTC (2,536 KB)
[v5]
Thu, 29 Oct 2026 20:56:25 UTC (1 KB) (withdrawn)
来源：arXiv cs.AI · arxiv.org