AlphaProof Nexus：AI 自动证明数学研究级开放问题

核心问题

LLM 在数学推理上越来越强，但生成自然语言证明不可靠——隐含的逻辑错误会级联传播，导致人类审稿成本极高。现有方案用 Lean 等形式化语言让编译器自动验证，但之前成功仅限于竞赛数学和辅助形式化人类已有的证明。在研究级开放问题上，AI 形式化证明到底能做到什么程度？ 这是本文第一次大规模系统性回答的问题。

系统架构

AlphaProof Nexus 的核心是 LLM 子智能体循环"生成证明草稿 → Lean 编译器验证 → 反馈修正"，并用进化算法协调多个子智能体的搜索。系统有四个递进版本：Agent A（基础 LLM + Lean 验证）→ Agent B（+ AlphaProof 工具）→ Agent C（+ 进化搜索 + Elo 评分）→ Agent D（全功能，AlphaProof + 进化）。

图：全功能 AlphaProof Nexus 智能体设计。LLM prover 子智能体精化证明草稿，可选调用 AlphaProof；进化算法用 Elo 评分筛选草稿种群驱动搜索。

证明过程的关键设计是"草稿精化"——子智能体不断修改 Lean 文件中的证明骨架，调用 AlphaProof 解决子目标，从失败中积累经验注释到草稿上，供下一次尝试参考。

主要成果

图：AlphaProof 智能体的输入输出示例（Erdős #125）。用户提供带 sorry 占位符的 Lean 文件，智能体推理并调用工具完成证明。

Erdős 问题9/353 — 在 Formal Conjectures 仓库中的 353 个 Erdős 开放上运行，解决了 9 个，包括两个悬而未决 56 年的难题（#12(i) 和 #125）。每个问题推理成本仅数百美元。

OEIS 猜想44/492 — 用 Gemini 自动将 492 个 OEIS 开放问题形式化为 Lean 语句，AI 证明了其中 44 个之前未被证明的猜想。

多领域突破凸优化（证明 Anchored GDA 精确收敛率 + 发现新参数调度）、代数几何（15 年 Hilbert 函数开放问题）、图论（Graffiti 1996 年猜想）、加法组合（Ben Green 问题列表 #57）、量子光学（单色量子图存在性）。

关键发现：简单 loop 的惊人力量

图：四类智能体在 Erdős 问题上的求解率 vs 推理成本（USD）。基础 Agent A 竟然也解决了全部 9 个问题，只是在难题上成本更高。

最基础的 Agent A（纯 LLM + Lean 验证循环）居然也解决了全部 9 个 Erdős 问题，只是在最难的问题上成本更高。这说明随着 LLM 能力提升，"编译器反馈驱动 LLM 推理"这个简单 loop 的威力被低估了。全功能 Agent D 的优势主要体现在最难的问题上（成本降低 2-5 倍），但差距在缩小。单独的 AlphaProof 树搜索和更小的模型都无法解决任何一个问题。

失败模式与局限

成功集中在 Lean 数学库成熟的领域（组合、优化、数论），大多数 Erdős 问题仍无法触及。两个典型失败模式：(1) 把核心困难"外包"给一个 sorry 占位符引理（本质是换个方式重述目标）；(2) 幻觉引用不存在的文献引理。这恰恰说明了端到端形式化验证的不可替代性。

趋势判断

这篇文章指向一个清晰的走向：随着 LLM 能力增强，从"训练专用 RL 系统"转向"简单 agentic loop + 形式化验证反馈"正在成为数学 AI 的主路径。编译器反馈是最强的 grounding 机制。进化搜索和 AlphaProof 在最难问题上仍有价值，但差距在快速缩小。形式化 AI 的价值不仅是"解决问题"，更在于帮助人类发现形式化错误、加深对问题结构的理解。