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

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.

scadnano: A browser-based, scriptable tool for designing DNA nanostructures

We introduce $\textit{scadnano}$ (https://scadnano.org) (short for "scriptable cadnano"), a computational tool for designing synthetic DNA structures. Its design is based heavily on cadnano, the most widely-used software for designing DNA origami, with three main differences: 1. scadnano runs entirely in the browser, with $\textit{no software installation}$ required. 2. scadnano designs, while they can be edited manually, can also be created and edited by a $\textit{well-documented Python scripting library}$, to help automate tedious tasks. 3. The scadnano file format is $\textit{easily human-readable}$. This goal is closely aligned with the scripting library, intended to be helpful when debugging scripts or interfacing with other software. The format is also somewhat more expressive than that of cadnano, able to describe a broader range of DNA structures than just DNA origami.