Datasets

OpenATP provides utilities to download common proof-synthesis benchmarks (see Downloading a dataset). The available datasets are listed in the DATASET enum. We list each in the table below.

Benchmark	DATASET	Toolchain	Paper	Source
Examples	EXAMPLES	v4.28.0	—	API
PutnamBench	PUTNAM	v4.27.0	Tsoukalas et al. [7]	GitHub
FATE-H	FATE_H	v4.28.0	Jiang et al. [4]	GitHub
FATE-M	FATE_M	v4.28.0	Jiang et al. [4]	GitHub
FATE-X	FATE_X	v4.28.0	Jiang et al. [4]	GitHub

Warning

PutnamBench pins an older version of Lean than the default image. A custom skeleton must be supplied to tasks_from_dir() and the Docker image must be rebuilt with version v4.27.0 of Lean and Mathlib as well.