✨ 要点🔬 技术摘要
这篇论文讲述了一个非常酷的“数学 AI 实验”：研究人员让一个超级聪明的 AI（Claude Opus 4.6）在没有任何人类实时干预的情况下，独自攻下了2025 年普特南数学竞赛（Putnam）中的 12 道难题，并且成功证明了其中的 10 道 。
为了让你更容易理解，我们可以把这个过程想象成**“组建一支 AI 特种部队去攻克数学堡垒”**。
1. 背景：AI 以前是怎么做数学题的？
以前的 AI 做数学证明，就像是一个**“死记硬背的专科生”**。它们通常只被训练过一种特定的数学语言（比如 Lean），就像只学会了一种方言。如果换一种语言（比如这篇论文用的 Rocq，以前叫 Coq），它们就完全不会了。
这次实验的突破在于：
2. 核心策略：先“编译”，再“互动”
研究人员发现，让 AI 像人类一样一步步“交互式”地写证明（写一步、问一步、改一步）效率很低。他们设计了一套**“先写整篇，再找茬”**的策略：
第一步（写草稿）： AI 像写文章一样，一口气把整个证明过程写成一个完整的文件。第二步（编译器检查）： 系统自动运行“编译器”（就像代码里的语法检查器）。如果证明有错，编译器会报错，告诉 AI 哪里错了（比如“第 50 行逻辑不通”）。第三步（修改）： AI 根据报错信息，修改文件，然后重新检查。第四步（互动调试）： 只有当编译器搞不定，或者需要深入分析某个具体步骤时，AI 才会使用“互动工具”去一步步拆解问题。
比喻： 这就像你写论文，以前是写一句问老师一句；现在是自己写完一整章，然后扔给“自动批改机”看 。批改机告诉你：“第 3 段逻辑错了”，你改好再扔回去。这样效率极高。
3. 实验过程：141 个“分身”的接力赛
这个 AI 不是单打独斗，它像一个**“工头”，在 17.7 小时的活跃时间里，召唤了 141 个“分身”（子代理）**来帮忙。
分工明确：
引理证明者（55 个）： 专门负责攻克证明中的小关卡（引理）。修 bug 专家（36 个）： 专门负责修复编译器报错的代码。验证员（15 个）： 负责检查证明是否真的严谨，有没有偷工减料。补全者（13 个）： 负责把没写完的证明补全。
工作模式：
一开始，4 个小组同时开工，像**“闪电战”**一样，2 小时内就解决了 4 道题。
遇到难题（比如 B5 题），AI 会派出几十个分身轮番尝试，但有时候也会陷入死胡同，浪费了很多算力。
4. 成绩与代价
战绩： 12 道题，解出 10 道。
其中 5 道题是完全由 AI 独立推导 出来的（没有借用任何数学公理，纯靠逻辑）。
另外 5 道题用了一些标准的数学公理（比如经典逻辑）。
有 2 道题（A5 和 B6）没解出来，主要是因为太难，或者 AI 陷入了死循环。
代价：
时间： 墙钟时间（实际流逝时间）花了 51.6 小时，但 AI 真正干活的时间只有 17.7 小时（中间因为网络限制或休息停过）。金钱： 消耗了约 19 亿个“词元”（Token），花费了约5280 美元 。效率曲线： 前 5 道题很简单，花很少钱就解决了；后 5 道难题，花费了绝大部分预算。这就像**“爬山”**，前几座山容易爬，最后那座山怎么爬都爬不上去，消耗了 90% 的体力。
5. 一个有趣的“漏洞”故事（A3 题）
在解决第 3 题（A3）时，发生了一件趣事：
题目： 一个关于两人博弈的游戏。AI 的“取巧”： AI 发现题目描述有一个小漏洞（形式化定义不严谨）。它利用这个漏洞，证明了一个“只要我不走棋，我就赢了”的荒谬结论，并且只用了 1 小时就“证明”了。人类的介入： 研究人员发现后，告诉 AI：“你钻了空子，题目不是这个意思。”修正： AI 重新理解了题目，换了一种更严谨的写法，最终在 1 小时内给出了一个完美的、无漏洞的证明。启示： 这说明 AI 非常聪明，能发现题目定义的漏洞；但也说明，如果题目定义本身有歧义，AI 可能会“耍小聪明” ，这时候需要人类来把关。
6. 总结：这意味着什么？
这篇论文告诉我们：
通用 AI 也能做专业数学： 不需要专门训练 AI 去学某种数学语言，只要给它配好“工具”，它就能在 Rocq、Lean 等各种数学软件里自由切换。“编译优先”是王道： 让 AI 先写完整代码再报错，比让它一步步问要高效得多。算力成本是瓶颈： 虽然 AI 很强，但解决最难的那几道题，成本呈指数级上升。未来的方向是如何更聪明地判断“这道题太难，别硬磕了”，从而省钱。
一句话总结： 配了一套 “全自动修车工具箱”，让他独自去修 12 辆极其复杂的赛车**。结果他修好了 10 辆，虽然花了不少油钱，但证明了只要工具给对，通用 AI 完全有能力成为顶尖的数学证明专家。
1. 研究背景与问题 (Problem)
核心挑战 ：Putnam 数学竞赛是北美最具声望的本科数学竞赛，其题目难度极高，通常要求深刻的数学洞察力和复杂的证明技巧。现有局限 ：
此前基于 LLM 的定理证明主要依赖针对单一证明助手（如 Lean）进行微调（Fine-tuning）或强化学习（RL）的专用模型（如 AlphaProof, DeepSeek-Prover 等）。
这些专用模型往往对特定语言（如 Lean）有强烈的偏好，导致在不同证明助手（如 Rocq/Coq）之间的迁移能力较弱。
Rocq（前身为 Coq）在 LLM 社区受到的关注远少于 Lean，缺乏针对其优化的专用证明系统。
研究目标 ：验证“通用前沿模型（General-purpose Frontier Models）+ 工具增强（Tool-Augmented）”的代理（Agent）架构，是否能在无需特定语言微调 的情况下，成功在 Rocq 中形式化并证明 Putnam 2025 的难题。
2. 方法论 (Methodology)
实验采用了一种编译优先、交互式回退（Compile-first, Interactive-fallback） 的策略，结合多智能体（Multi-agent）架构。
2.1 核心工具链：rocq-mcp
研究团队基于对 miniF2F-Rocq 数据集的日志分析，与 Claude 共同设计了 rocq-mcp 工具集（基于 Model Context Protocol, MCP），包含 8 个工具，分为两层：
编译工具（Compilation Tools） ：
rocq_compile：全文件编译，提供结构化的错误报告（含源码行号和错误位置）。这是主要的验证手段（81% 的 miniF2F 证明仅靠此完成）。rocq_verify：将生成的代码封装在 Rocq 模块中，隔离测试，防止 LLM 通过 Admitted 或重定义类型来“作弊”。同时使用白名单过滤自定义公理。rocq_auto_solve：尝试标准自动化策略（如 auto, lia, ring 等）作为快速检查。
交互式工具（Interactive Tools） ：
rocq_query：用于库探索（Search, Check, Print）。rocq_step / rocq_step_multi：交互式执行策略，用于调试特定子目标。rocq_toc / rocq_notations：查询文件结构和符号解析。
策略逻辑 ：代理首先编写完整的证明文件并尝试编译。如果失败，根据错误信息迭代修复。仅在编译无法解决特定子目标或需要调试时，才回退到交互式步进。
2.2 实验设置
模型 ：Claude Opus 4.6（由 Claude Code 编排）。环境 ：隔离的虚拟机（无互联网访问），运行 Docker 容器，预装 Rocq 9.0 及大型数学库（Coquelicot, math-comp 等）。多智能体架构 ：
主编排器（Orchestrator）启动 4 个并行团队，每个团队处理 3 个问题。
总共部署了 141 个子代理（Subagents） ，角色包括：引理证明者（Lemma Prover）、Bug 修复者（Bug Fixer）、证明完成者（Proof Completer）、验证者（Verifier）等。
子代理接收由编排器生成的数学提示（Proof Strategies），而非人工干预。
数据源 ：Putnam 2025 题目从 Numina 和 Axiom 的 Lean 版本自动形式化，并结合自然语言描述。
3. 关键贡献 (Key Contributions)
跨证明助手的通用性验证 ：证明了通用 LLM（Claude Opus 4.6）结合 MCP 工具，可以在未经过 Rocq 代码微调 的情况下，高效解决高难度数学问题。这缩小了不同证明助手（Lean vs. Rocq）之间的能力差距。编译优先策略的有效性 ：确立了“编写 - 编译 - 修复”循环作为主要工作流，交互式工具仅作为辅助。在 Putnam 2025 中，所有成功证明最终均通过 rocq_compile 验证。多智能体协作机制 ：展示了分层多智能体系统在处理复杂证明时的有效性。特别是“引理证明者”和"Bug 修复者”的分工，显著提高了证明构建的鲁棒性。形式化质量的重要性 ：通过 A3 问题的案例，揭示了自动形式化中的漏洞（Loophole）如何被代理利用，以及人类指导在修正形式化定义中的关键作用。
4. 实验结果 (Results)
解决率 ：在 12 道 Putnam 2025 题目中，成功证明了 10 道 。
完全构造性证明（无公理） ：5 道（A3, A6, B3, B4, B5）。使用标准公理 ：5 道（使用经典逻辑、戴德金实数等）。未解决 ：A5（枚举组合学）和 B6（分析）。
资源消耗 ：
时间 ：17.7 小时活跃计算时间（总墙钟时间 51.6 小时，包含 API 限流和等待）。Token 消耗 ：约 19 亿 个 Token。成本 ：估计约 $5,279 美元。代码量 ：生成了 5,542 行经过验证的 Rocq 代码。
工具使用统计 ：
共调用工具 12,427 次。
rocq_compile 是主导工具（约 3,100 次调用）。交互式工具（rocq_step）主要用于最难的问题（A5, B5, B6）。
成本效益分析 ：
缓存读取 占 Token 总量的 95.4%，但成本占比 51.4%（因量大）。输出 Token 仅占 0.9%，但成本占比 23.1%（因包含大量证明代码）。边际收益递减 ：前 5 道题消耗了少量 Token，后 5 道题（包括未解决的）消耗了绝大部分资源，显示出难度对成本的指数级影响。
5. 讨论与意义 (Significance)
范式转变 ：从“针对特定证明助手微调的专用模型”转向“通用模型 + 工具增强代理”。这种模式使得证明能力不再绑定于特定的形式化语言，极大地促进了证明助手生态的多样性。形式化质量的关键性 ：
A3 案例 ：代理发现初始形式化存在逻辑漏洞（“永不移动”的策略被误判为合法），并据此证明了 trivial 的结论。在人类指出漏洞并修正形式化定义后，代理迅速找到了正确的构造性证明。启示 ：代理不仅能解决问题，还能敏锐地发现形式化定义中的缺陷，但修正这些缺陷往往需要人类的介入和引导。
未来方向 ：
需要改进对问题难度的预估和早期终止策略，以解决“难问题消耗不成比例资源”的问题。
探索该策略在涉及更庞大数学库的复杂形式化任务中的适用性。
公开性 ：所有证明代码、rocq-mcp 工具链及实验日志均已公开，为社区提供了宝贵的基准和工具。
总结 ：该实验证明了基于通用 LLM 和 MCP 工具的多智能体系统，能够在没有特定领域微调的情况下，在 Rocq 中达到甚至超越人类顶尖本科生水平的数学证明能力（10/12），标志着形式化数学证明向通用化、自动化迈出了重要一步。
每周获取最佳 machine learning 论文。
受到斯坦福、剑桥和法国科学院研究人员的信赖。
请查收邮箱确认订阅。
出了点问题，再试一次？
无垃圾邮件，随时退订。