cs.LGMar 20, 2026

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

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

Organizations: IRIF, Université Paris Cité, Inria, CNRS · DI ENS, PSL University, Inria · PRGM DEV

Read PDF
Ask AI
Cite

Copy citation

DOINot available for this paper

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.

Figures & tables

ProblemStatusLinesTimeAxiomsDomain
A1✓30551mclassicalNumber theory
A2✓3081h 33mRealsReal analysis
A3✓1101h 07mNoneCombinatorics
A4✓5314h 58mRealsLinear algebra
A5✗2294––Enum. combinatorics
A6✓89719h 56mNoneNumber theory
Table 1: Per-problem results. Lines = lines of Rocq code. Time = wall-clock from experiment start to successful compilation. ✓ = exploited a loophole in the A3 formalization (later fixed by the agent). Bold None = fully constructive (zero axioms).
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.
ToolCallsRole
rocq_compile∼\sim 3,100Compilation
rocq_verify∼\sim 120Axiom checking
rocq_auto_solve∼\sim 20Quick automation
rocq_query∼\sim 80Library search
rocq_step∼\sim 450Interactive debug
Table 2: MCP tool usage.
RoleAgentsTokensTool calls
Lemma Prover55738M4,845
Bug Fixer36538M3,409
General21253M1,588
Verifier1565M639
Proof Completer13185M1,257
Compiler11M14
Table 3: Subagent roles. Roles are inferred from each agent’s initial prompt.
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.
CategoryTokens%Cost% Cost
Input<< 1M0.0%$10.1%
Output16M0.9%$40623.1%
Cache creation72M3.8%$44825.5%
Cache read1,809M95.4%$90551.4%
Total1,897M100%$1,760100%
Table 4: Token economics.
GroupProblemsActive timeEst. tokens
Easy (A1, A2, A3, B4)4<< 2h∼\sim 100M
Medium (A4, B1, B2, B3)4∼\sim 5h∼\sim 400M
Hard (A6, B5)2∼\sim 11h∼\sim 600M
Unsolved (A5, B6)2–∼\sim 800M
Table 5: Scaling behavior by problem difficulty. The unsolved problems consumed the most resources.
More in this topic

Large Language Model-Guided Theorem Proving

See all 40 papers

Explore similar work

CardsList

  1. Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean

    Sep 30, 2026Jules Viennot, Guillaume Baudart, Marc LelargeAutomated Theorem ProvingEvolutionary Optimization

    IRIF, Universit´e Paris Cit´e, Inria, CNRS · DI ENS, PSL University, Inria

  2. SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

    Oct 6, 2026Hanchao Zhou, Jialei LiLarge Language Model-Guided Theorem ProvingAutomated Theorem Proving

  3. PrologMCP: A Standardized Prolog Tool Interface for LLM Agents

    Jun 12, 2026Agnieszka Mensfelt, Adarsh Prabhakaran, Adrian Haret +2Logic ProgrammingSymbolic Reasoning

    Department of Computer Science, Royal Holloway, University of London, UK