AxiomProver 是一个能生成可被机器验证的数学证明的AI系统。它由初创公司 Axiom 开发，创始人是一位名叫洪乐潼（Carina Hong）的25岁华裔科学家。

它和普通AI的核心区别在于：

1. 工作原理：语言与验证器结合

普通大语言模型（如ChatGPT）的本质是预测“下一个最可能的词”，导致它可能会“一本正经地胡说八道”（即幻觉）。

而AxiomProver采用双保险机制：

• 生成器：由大模型负责提出证明思路。
• 验证器：使用名为 Lean 的编程语言来检查。Lean就像一个铁面无私的“裁判”，必须逻辑上零误差才能通过。如果证明有瑕疵，机器自己就会立刻驳回。

2. 核心优势：效率和可靠性

• 极致效率：曾实现“上午10点丢给系统一个难题，下午4点就拿到完整证明”。
• 绝对准确：正确性交给机器验证，彻底消除了人工审稿可能出现的疲劳或看走眼的风险。

3. 关键战绩

该系统已在国际顶尖数学舞台证明了自己：

• 满分攻克普特南竞赛：在被称为“北美最难本科生数学竞赛”的普特南（Putnam）中，拿下120分满分（最佳人类得分110分）。
• 解决长期难题：解决了Chen-Gendron猜想等困扰学界多年的难题。
• 产出顶会论文：已有多篇由它生成的论文被权威数学期刊接收。

AxiomProver 如何应用 python ？

AxiomProver 和 Python 的关系，更像一个由核心引擎（Lean）+ 智能大脑（AI）+ Python工具箱组成的完整体系。你可以通过官方提供的三种主要方式，在你的 Python 环境里调用它的能力。

🔧 方式一：官方 Python 工具包

Axiom 官方为开发者提供了几个开箱即用的 Python 包，推荐从这些项目开始。

• ax-prover-base: 一个用 Python 编写的最小化代理，可以直接集成到你的 Python 项目里，负责与底层的 Lean 证明器交互，发起证明请求和处理结果。
• ax-mcp: 一个用 Python 实现的 MCP (Model Context Protocol) 服务器，让使用该协议的语言模型能以标准化方式调用 Lean 环境进行定理证明。
• axiomatic-python-sdk: Axiom 官方提供的 Python SDK，封装了其 API 细节，让你的 Python 代码能更方便地进行身份验证和发起请求。

🔌 方式二：通过 MCP 协议整合

MCP (Model Context Protocol) 是所有工具的核心接入点。AxiomProver 给大模型提供了一整套 Lean 开发工具，并通过 lean-lsp-mcp 项目向外界提供标准接口。

你可以通过 ax-mcp 服务器，让任何支持该协议的 AI 模型获得以下能力：

• 项目管理: 编译和构建 Lean 项目，读取项目文件等。
• 调试反馈: 实时检查代码编译错误，获取当前证明目标状态，查看提示信息等。
• 代码辅助: 获取自动补全建议，自动尝试多种证明方法，直接在 Lean 环境中执行代码。
• 搜索推理: 在数学库 Mathlib 中按类型签名搜索引理，快速查找定理，利用自动化定理证明工具辅助推理等。

💻 方式三：API 与 CLI 工具

你还可以通过 Axiom 的云端 API 和命令行工具（CLI），在 Python 程序中集成其证明能力。不过需要注意，目前 API 仅向受邀用户开放。

如果想了解申请通道，建议访问 Axiom API Console。获得 API Key 后，就可以用 Python 调用官方 SDK 或直接通过 CLI 来使用 Axiom Proving API 了。

🧪 实战示例与开源案例

Axiom 官方在 GitHub 上开源了一些具体项目，是极佳的学习资料。例如，AgreeToDisagree 仓库就完整展示了其形式化证明的输入输出流程。

🤔 常见问题（FAQ）

• AxiomProver 本身是用 Python 开发的吗？
  不，其核心引擎是 Lean 4，但整个系统集成了多种技术，Python 是它官方支持和推荐的开发接口语言之一。

• 我必须付费才能使用吗？
  API 服务当前是邀请制，未来可能会推出商业付费计划。但所有的官方 Python 工具包都是开源免费的，你可以下载本地部署和学习。

• 用它能做什么？
  很适合在项目中集成可靠的数学推理能力，比如自动检测和修复算法漏洞、生成可验证的金融风控模型证明，或者作为AI Agent 的数学知识库后端。

• 我可以从哪个项目开始？
  官方强烈推荐从 ax-prover-base 项目入手。这是一个用 Python 编写的“最小化代理”，虽然功能精简，但能让你在 Python 环境中，低成本地体验核心的自动定理证明流程。