mlsanityData to 7 Oct 2026

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

arXiv 2603.20405 ↗First posted 20 Mar 2026cs.LG cs.CL cs.LOcited by 0

Not on the map. Why?

Abstract (arXiv)

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.

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 6 of its 15 references that are in the map. First posted on arXiv 20 Mar 2026.

Builds on

6 of 15 references.

References · 6

  1. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  2. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  4. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  5. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  6. 2025MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Studycited by 5

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2026Growing an Agent/Prover Interface: Evolutionary Tool Design for Cost-Efficient Theorem Proving in Rocq and Lean
  2. 2024MCP-Solver: Integrating Language Models with Constraint Programming Systems
  3. 2026Cogentic: Multi-Agent Orchestration for Automated Proof Discovery
  4. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving
  5. 2026Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
  6. 2026Understanding CDCL Solvers via Scalability Studies and Proofdoors ↗
  7. 2026Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs
  8. 2026RocqSmith: Can Automatic Optimization Forge Better Proof Agents?