AI用工具链自主解出10道普特南数学竞赛题，证明效率超预期。
Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
- 用MCP工具链实现先编译后交互的策略，自动调用子代理求解。
- 在无网络环境下17.7小时算力内完成10道题，消耗约19亿token。
- 适合关注AI数学推理、自动化证明及智能工具链的研究者。
我们报告了一项实验：配备模型上下文协议（MCP）工具集的Claude Opus 4.6，在Rocq证明助手环境中，自主完成了2025年普特南数学竞赛12道题中的10道。MCP工具由Claude基于先前miniF2F-Rocq实验的日志分析设计，采用“先编译、后交互”策略。实验在隔离虚拟机中运行，无互联网访问，共部署141个子代理，活跃计算耗时17.7小时（墙钟时间51.6小时），消耗约19亿个标记（tokens）。所有证明均已公开。
原文摘要 · Abstract (English)
We report on an experiment in which Claude Opus~4.6, equipped with a suite of Model Context Protocol (MCP) tools for the Rocq proof assistant, autonomously proved 10 of 12 problems from the 2025 Putnam Mathematical Competition. The MCP tools, designed with Claude by analyzing logs from a prior experiment on miniF2F-Rocq, encode a "compile-first, interactive-fallback" strategy. Running on an isolated VM with no internet access, the agent deployed 141 subagents over 17.7 hours of active compute (51.6h wall-clock), consuming approximately 1.9 billion tokens. All proofs are publicly available.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。