Mizar

该数据集包含57,917个定理，其中特别关注了一部分包含32,524个定理的数据子集，这些定理附有相应的自动定理证明（ATP）证明，用于前提选择。该数据集被划分为训练集（80%）、开发集（10%）和测试集（10%）。在训练、开发和测试中使用的定理数量为32,524个，所执行的任务是前提选择。

This dataset encompasses 57,917 theorems overall, with a particular emphasis on a subset of 32,524 theorems. Each theorem within this subset is paired with corresponding Automated Theorem Proving (ATP) proofs, and this subset is tailored for premise selection tasks. The subset is partitioned into three standard splits: 80% for training, 10% for development, and 10% for testing. A total of 32,524 theorems are utilized across these training, development, and test splits, and the core task addressed by this dataset is premise selection.