PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition

TL;DR

PutnamBench is a challenging new benchmark with formalized competition math problems in multiple proof assistants, designed to evaluate neural theorem-provers' capabilities on undergraduate-level mathematics.

Contribution

It introduces a comprehensive, multi-language benchmark of formalized competition problems, providing a new standard for evaluating neural theorem-provers.

Findings

Existing neural theorem-provers solve only a few problems

PutnamBench is a difficult open challenge for AI research

The benchmark covers broad undergraduate mathematics topics

Abstract

We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692 hand-constructed formalizations of 640 theorems sourced from the William Lowell Putnam Mathematical Competition, the premier undergraduate-level mathematics competition in North America. All the problems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. PutnamBench requires significant problem-solving ability and proficiency in a broad range of topics taught in undergraduate mathematics courses. We use PutnamBench to evaluate several established neural and symbolic theorem-provers. These approaches can only solve a handful of the PutnamBench problems, establishing the benchmark as a difficult open challenge for research on neural theorem-proving. PutnamBench is available at https://github.com/trishullab/PutnamBench.