Claude Opus 4.6 + Rocq-MCP 在隔离环境中自主证明 2025 Putnam 12 题中的 10 题

Baudart、Lelarge、Stérin 与 Viennot 为 Rocq proof assistant 构建 MCP tools，让 Claude Opus 4.6 在隔离 VM、无互联网环境下自主证明 2025 Putnam 的 10/12 题。系统使用 compile-first / interactive-fallback 策略，部署 141 个 subagents，消耗约 17.7 小时 active compute、1.9B tokens；所有 proofs 公开。