Ax-Prover：面向数学与量子物理的定理证明多智能体框架

Ax-Prover 用 MCP 接 Lean 工具做多领域定理证明，新基准上领先。

资讯摘要

论文提出 Ax-Prover，一个在 Lean 中自动证明定理的多智能体系统，可自主运行或与人类专家协作。它通过 Model Context Protocol（MCP）为 LLM 接入 Lean 工具，兼顾推理与形式正确性。作者在两个公开数学基准及新提出的抽象代数、量子理论 Lean 基准上评测：公开数据集上与先进证明器相当，新基准上明显领先；并展示其辅助数学家形式化密码学定理的用例。

要点速读

1. Ax-Prover 通过 MCP 为 LLM 提供 Lean 工具，以形式化证明方式求解科学问题。
2. 在两个公开数学基准上与前沿 LLM 和专用证明器对比，表现相当。
3. 在作者新提出的抽象代数与量子理论 Lean 基准上大幅领先，并演示辅助专家形式化密码学定理。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/3 08:00:27（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。