FormalMATH, where the Lite subset is taken as the test set, and the remaining examples are taken as the train set.
import datasets
data_lite = datasets.load_dataset("SphereLab/FormalMATH-Lite", split='train')
data_full = datasets.load_dataset("SphereLab/FormalMATH-All", split='train')
filter out the lite theorems from the full dataset
lite_theorems = set(data_lite['theorem_names'])
data_full_not_lite = data_full.filter(lambda x: x['theorem_names'] not inlite_theorems)
assert 0 <… See the full description on the dataset page:
https://huggingface.co/datasets/ricdomolm/FormalMATH.
