Coq’s standard library

该数据集是专为评估机器学习在Coq领域的应用而设计的一个标准数据集，它包含了由Coq专家精心打造并经过数十年优化的证明。在转移理论学习设置中，该数据集采用了不同的Coq理论进行训练、验证和测试，以模拟整数线性规划（ILP）在实际应用中的情况。该数据集的规模包括41个理论和151,678个证明状态，其任务是预测交互式定理证明的战术。

This is a standard dataset specifically designed for evaluating machine learning applications in the field of Coq. It contains proofs carefully crafted by Coq experts and optimized over decades. In a transfer learning setup, this dataset utilizes distinct Coq theories for training, validation and testing to simulate real-world application scenarios of Integer Linear Programming (ILP). The dataset includes 41 theories and 151,678 proof states, with the task being the prediction of tactics for interactive theorem proving.