Claude Opus 4.6, equipped with MCP tools for the Rocq proof assistant, autonomously proved 10 of 12 problems from the 2025 Putnam Mathematical Competition. No internet access. No human guidance during execution. 141 subagents across 17.7 hours of active computation and 51.6 hours of wall time. Approximately 1.9 billion tokens consumed.
The methodology matters more than the score. The researchers designed tools using a compile-first, interactive-fallback strategy — try to compile the proof directly; if that fails, enter an interactive proof mode. The agent ran on an isolated virtual machine, formalized each problem in Rocq, and produced machine-checked proofs. All proofs are publicly available.
The Putnam is the most prestigious undergraduate mathematics competition in North America. Its problems are selected for difficulty, requiring creative insight rather than mechanical application of known techniques. The median score for participants is typically 0 or 1 out of 120 points. Top scorers solve 4-6 problems. This agent solved 10.
Two structural observations. First: the strategy is formal verification, not answer generation. The agent doesn't guess answers and check them. It constructs proofs in a formal language where every step must be mechanically verified. The proof assistant is the oracle — not the LLM's confidence, not pattern matching against training data, but the compiler's judgment of logical validity. The LLM proposes; Rocq disposes.
Second: the resource cost. 1.9 billion tokens is roughly 1,000 times what a human solver would “consume” in working memory during the same competition. The compute isn't cheap. But the proofs are machine-checked — they're correct in a way that human Putnam solutions, even correct ones, aren't formally guaranteed to be.
The two unsolved problems remain uncharacterized in the abstract. Whether they failed due to formalization difficulty (translating the problem into Rocq), search exhaustion (running out of proof strategies), or genuine mathematical hardness (the problem exceeds the model's reasoning capacity) would reveal different things about the boundary of AI mathematical reasoning.