[2603.20405] Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP

Computer Science > Machine Learning arXiv:2603.20405 (cs) [Submitted on 20 Mar 2026] Title:Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP Authors:Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot View a PDF of the paper titled Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP, by Guillaume Baudart and 3 other authors View PDF HTML (experimental) Abstract: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. Subjects: Machine Learning (cs.LG); Computation and Language (cs.CL); Logic in Computer Science (cs.LO) Cite as: arXiv:2603.20405 [cs.LG]   (or arXiv:2603.20405v1 [cs.LG] for this version)   https://doi.org/10.48550/arXiv.2603.20405 Focus to learn more arXiv-issued DOI via DataCite (pending registration) Submission history From: Guillaume Baudart [view email] [v1] Fri, 20 Mar 2026 18:25:42 UTC (63 KB) Full-text links: Access Paper: View a PDF of the paper titled Putnam 2025 Problems in Rocq using Opus 4.6 an...