July 23, 2026
How we solved PutnamBench
A look at formally proving undergraduate competition mathematics
To stress-test our upcoming Isabelle-based verification platform, we pointed Varto Cloud at the PutnamBench benchmark. The Putnam Mathematical Competition is an annual undergraduate mathematics competition, and PutnamBench is a collection of its problems formalized for theorem provers.
Varto solved all 640 Isabelle formalizations. This marks the first Isabelle submission and the first submission to solve an entire benchmark category. This makes Varto the undisputed number one in the Isabelle category.
We also auto-formalized every problem missing from the Isabelle category. These formalizations are currently under review by the benchmark maintainers. Varto proved all of them as well.
Token cost per target
- Minimum
- < $1
- Median
- $6
- Maximum
- $67
Proof time per target
- Minimum
- < 2 min
- Median
- 14 min
- Maximum
- 121 min
We used GPT-5.5, with most proofs completed at medium or high reasoning effort.
Our average token cost per problem was $8, and our average proof time was 16 minutes. That is about 8× cheaper and 23× faster than the top-ranked Lean submission as of July 20, 2026.
We attribute the low token cost and proof time primarily to Varto’s self-learning skills, Isabelle’s advanced built-in proof tactics, and the Archive of Formal Proofs.