PutnamBench

该数据集名为PutnamBench，包含了1692个手工构建的形式化证明，这些证明源自北美顶级本科数学竞赛——威廉·洛厄尔·普特南数学竞赛中的640个定理。这些形式化证明以Lean 4、Isabelle以及部分以Coq语言编写，为当前的定理证明方法带来了重大挑战。该数据集的规模为1692个形式化证明，覆盖了640个定理。其任务旨在评估神经定理证明器解决竞赛数学问题的能力。

The dataset is named PutnamBench, which contains 1692 hand-constructed formal proofs derived from 640 theorems in the William Lowell Putnam Mathematical Competition—a top-tier undergraduate mathematics competition in North America. These formal proofs are written in Lean 4, Isabelle, and partially in Coq, posing significant challenges to current theorem proving methods. Comprising 1692 formal proofs covering 640 theorems, the core task of this dataset is to evaluate the capabilities of neural theorem provers in solving competitive mathematical problems.