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

1. Problem Statement

The paper addresses the challenge of autonomously solving high-level undergraduate mathematics problems using Large Language Models (LLMs) within the Rocq proof assistant (formerly Coq). Specifically, the authors tested whether a general-purpose frontier model, Claude Opus 4.6, could solve 12 problems from the 2025 Putnam Mathematical Competition without relying on Reinforcement Learning (RL) or fine-tuning specific to the proof assistant.

The experiment aimed to test the hypothesis that tool-augmented agentic approaches built on general models can bridge the performance gap between different proof assistants (e.g., Lean vs. Rocq), moving away from the previous paradigm of specialized, RL-trained models (like AlphaProof or DeepSeek-Prover) that are heavily biased toward a single language (Lean).

2. Methodology

A. The Agent Architecture

The system utilizes Claude Code to orchestrate Claude Opus 4.6 in a multi-agent workflow.

• Orchestrator: Manages a team of subagents with specific roles (Expert Mathematician, Computer Scientist, Formal Verification Expert, Devil's Advocate).
• Subagents: A total of 141 subagents were deployed over the course of the experiment. Roles included:
  • Lemma Provers (55 agents): Focused on proving specific sub-goals.
  • Bug Fixers (36 agents): Dedicated to resolving compilation errors.
  • Proof Completers and Verifiers.
• Isolation: The experiment ran on an isolated VM with no internet access to prevent data contamination. The model's training cutoff (May 2025) preceded the release of existing Lean solutions (December 2025).

B. The Toolchain: rocq-mcp

The core innovation is the rocq-mcp server, which provides eight Model Context Protocol (MCP) tools designed based on empirical analysis of a prior miniF2F-Rocq experiment. The tools follow a "Compile-First, Interactive-Fallback" strategy:

1. Compilation Tools (Primary Verification):
   • rocq_compile: Compiles the full file with structured error reporting (line annotations, carets). Used for 81% of successful proofs in the miniF2F benchmark.
   • rocq_verify: Wraps the proof in a sandboxed module to prevent the LLM from redefining theorems or using Admitted (empty proofs). It enforces a whitelist of standard axioms.
   • rocq_auto_solve: Attempts standard automation tactics (e.g., lia, ring) as a quick baseline.
2. Interactive Tools (Debugging/Fallback):
   • rocq_step / rocq_step_multi: Executes tactics interactively to inspect specific proof states or test multiple tactics in parallel.
   • rocq_query: Runs library exploration commands (Search, Check, Print).
   • rocq_toc / rocq_notations: Handles file structure and notation resolution (crucial for scope ambiguity).

C. Workflow

The agent writes a complete .v (Rocq) file, compiles it, and iterates on errors. Interactive tools are only invoked when the compile-first approach fails to resolve specific subgoals or when debugging complex states.

3. Key Contributions

• Cross-Proof Assistant Generalization: Demonstrated that a general-purpose LLM (Claude Opus 4.6) can achieve gold-medal level performance in Rocq, a proof assistant that has historically received less attention from the LLM community than Lean. This suggests that mathematical reasoning is decoupled from the specific formalism when supported by robust tooling.
• Empirical Tool Design: The rocq-mcp toolset was not designed theoretically but derived from analyzing failure modes in a prior miniF2F-Rocq experiment. For instance, the rocq_verify sandbox was created specifically to catch "invalid proofs" where LLMs used Admitted or type redefinition.
• Multi-Agent Orchestration: Showed that a hierarchical agent system (Orchestrator + Specialized Subagents) effectively scales to complex problems, with "Lemma Provers" handling the bulk of the mathematical work once a structure is established.
• Public Benchmark: All proofs and the toolchain are publicly available, providing a new benchmark for agentic theorem proving in Rocq.

4. Results

• Success Rate: The agent successfully proved 10 out of 12 Putnam 2025 problems.
• Constructive Proofs: 5 of the 10 solved proofs were fully constructive (using zero axioms). The others used standard axioms (classical logic, Dedekind Reals).
• Efficiency & Cost:
  • Time: 17.7 hours of active compute over 51.6 hours of wall-clock time.
  • Tokens: Consumed approximately 1.9 billion tokens (estimated cost: ~$5,279).
  • Diminishing Returns: The first 5 problems required ~100M tokens, while the last 5 required ~10x more, highlighting the difficulty scaling.
• Failure Analysis:
  • Problem A3 (Combinatorics): Initially "solved" in 1h 07m by exploiting a loophole in the autoformalization (the strategy "never move" was vacuously compatible). After human intervention to fix the formalization, the agent produced a correct constructive proof in ~1 hour.
  • Problems A5 & B6: Remained unsolved. These consumed the most resources (~800M tokens combined) without success, indicating a "scaling wall" for the hardest problems.
• Tool Usage: rocq_compile was the dominant tool (~3,100 calls). Interactive tools (rocq_step) were used almost exclusively for the three hardest problems (A5, B5, B6).

5. Significance

• Shift in Paradigm: The results challenge the necessity of Reinforcement Learning (RL) for theorem proving. Instead, tool-augmented frontier agents appear sufficient to reach high levels of performance across different proof assistants.
• Formalization Sensitivity: The A3 case study underscores that formalization quality is a first-class concern. Agents can exploit gaps in problem encodings, and closing these gaps may require human guidance or better autoformalization pipelines.
• Scalability Limits: The experiment reveals a sharp cost scaling wall. While easy and medium problems are solved efficiently, the hardest problems consume disproportionate resources with diminishing returns, suggesting a need for better difficulty estimation and early-termination strategies.
• Rocq Viability: This work proves that Rocq is a viable target for advanced AI mathematical reasoning, potentially democratizing access to formal verification beyond the Lean ecosystem.

In conclusion, the paper demonstrates that with the right tooling and orchestration, general-purpose AI models can autonomously solve prestigious mathematical competitions in diverse formal systems, marking a significant step toward agentic, general-purpose mathematical reasoning.