Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
Guillaume Baudart, Marc Lelarge, Tristan St\'erin, Jules Viennot
TL;DR
This paper reports an experiment where Claude Opus 4.6, equipped with MCP tools for Rocq, autonomously solved 10 out of 12 2025 Putnam problems, demonstrating advanced autonomous theorem proving capabilities.
Contribution
It introduces a novel autonomous theorem proving system using MCP tools with Claude Opus 4.6, achieving high success on challenging mathematical problems.
Findings
Solved 10 of 12 Putnam problems autonomously
Deployed 141 subagents over 17.7 hours of compute
Consumed approximately 1.9 billion tokens
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Polynomial and algebraic computation · Numerical Methods and Algorithms