Datasetpublic

ChristianZ97/PutnamBench-lean4

PutnamBench — Lean 4 (672 problems) Lean 4 formalizations from PutnamBench, a benchmark of problems from the William Lowell Putnam Mathematical Competition (1962-2023). Converted from the official GitHub repository for convenient HuggingFace datasets access. Citation @article{tsoukalas2024putnambench, title={PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition}, author={George Tsoukalas and Jasper Lee and John Jennings and… See the full description on the dataset page: https://huggingface.co/datasets/ChristianZ97/PutnamBench-lean4.

sourceHugging Faceapache-2.0updated 6mo agoView on Hugging Face

0likes119downloads

Dataset Card

PutnamBench — Lean 4 (672 problems)

Lean 4 formalizations from PutnamBench, a benchmark of problems from the William Lowell Putnam Mathematical Competition (1962-2023).

Converted from the official GitHub repository for convenient HuggingFace datasets access.

Citation

bibtex

@article{tsoukalas2024putnambench,
  title={PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition},
  author={George Tsoukalas and Jasper Lee and John Jennings and Jimmy Xin
          and Michelle Ding and Michael Jennings and Amitayush Thakur
          and Swarat Chaudhuri},
  journal={arXiv preprint arXiv:2407.11214},
  year={2024}
}

Schema

Field	Type	Description
`problem_name`	`str`	Identifier, e.g. `putnam_1962_a1`
`formal_statement`	`str`	Full Lean 4 theorem (+ abbrevs), ending in `:= sorry`
`informal_statement`	`str`	English problem statement
`informal_solution`	`str`	Solution sketch or `"None."`
`tags`	`list[str]`	Categories: algebra, analysis, geometry, etc.
`split`	`str`	Always `"test"`

Usage

python

from datasets import load_dataset

ds = load_dataset("ChristianZ97/PutnamBench-lean4")
print(len(ds["test"]))  # 672
print(ds["test"][0]["problem_name"])

Source

Official repo: <https://github.com/trishullab/PutnamBench> License: Apache-2.0 (Lean 4 and Isabelle portions)