PutnamBench
We present a multilingual benchmark for formal-theorem proving of problems from the William Lowell Putnam Mathematical Competition.
How to run
$ npm i -g lettokenburn-cli$ ltb bench info putnambench
External harness. No Harbor adapter has been generated for this benchmark yet. `ltb bench info` prints the known links.
Runs happen on your machine with your own subscription; only the score summary is pushed. CLI docs
Scores
0 sourced entriesNo sourced scores recorded yet.
Every number links to where it was published. Low-confidence rows are muted and need per-cell verification.
Reproduced by the community
All runsAbout
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.