Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP

Guillaume Baudart, Marc Lelarge, Tristan Stérin, Jules Viennot

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.

Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP

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.
Paper Structure (14 sections, 3 figures, 5 tables)

This paper contains 14 sections, 3 figures, 5 tables.

Table of Contents

  1. Introduction
  2. Contamination risk.
  3. Outline.
  4. Background and Experimental Setup
  5. The rocq-mcp Toolchain
  6. Tool Design from miniF2F Analysis
  7. Experimental Protocol
  8. Results
  9. Analysis
  10. How effective are the MCP tools?
  11. How does the multi-agent architecture perform?
  12. How do costs scale with problem difficulty?
  13. Discussion
  14. Conclusion

Figures (3)

  • Figure 1: Cumulative problems solved over wall-clock time. Solid green segments indicate active compute; dashed red segments indicate inactivity (API rate limits or user absence). Shaded regions mark the 7 detected gaps ($>$30 min). The first 4 problems were solved within 2 hours; B5 was not solved until 46 hours into the experiment.
  • Figure 2: Cumulative problems solved vs. cumulative tokens consumed (log scale). The first 5 problems required $\sim$100M tokens; the last 5 required $\sim$10$\times$ more, illustrating sharp diminishing returns on harder problems.
  • Figure 3: Subagent efficiency. Each bubble represents one subagent (141 total, filtered to those with $>$10 tool calls). Position: tokens consumed vs. tool calls (both log scale). Size: duration. Color: problem assignment.