Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866917518688387072 |
|---|---|
| author | Baudart, Guillaume Lelarge, Marc Stérin, Tristan Viennot, Jules |
| author_facet | Baudart, Guillaume Lelarge, Marc Stérin, Tristan Viennot, Jules |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_20405 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP Baudart, Guillaume Lelarge, Marc Stérin, Tristan Viennot, Jules Machine Learning Computation and Language Logic in Computer Science 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. |
| title | Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP |
| topic | Machine Learning Computation and Language Logic in Computer Science |
| url | https://arxiv.org/abs/2603.20405 |