Ax-Prover：面向数学与量子物理定理证明的深度推理智能体框架
Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics
Ax-Prover 是一个基于 Lean 的多智能体定理证明系统，通过 MCP 为 LLM 配备 Lean 工具，可自主运行或与人类专家协作。在公开数学基准上它与 SOTA 证明器相当，在团队新提出的抽象代数与量子理论 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.MA · arxiv.org