Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP
DGX agentarXiv:2603.20405v2 Announce Type: replace-cross 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,