在大型语言模型和$Lean$等证明助手的帮助下, 自动化证明数学定理展现出了广阔的前景. 然而, 由于公开数据匮乏, 数据专业性强以及计算量庞大的问题, 形式化证明的机器学习方法面临瓶颈. 为了解决数据稀缺的问题, 本文构建了一个专注于组合数学的全新基准, 名为$Comlib$. 具体地, 首先通过$Lean$形式化证明了500 多个新定理, 其中包括吸收定理, 并行求和等多个经典组合数学定理. 在此基础上, 本文提出了一种融合搜索和预测的数据增强方法, 进一步扩大了基准的数据量. 在一组标准基准上进行了对比评估所提出的数据增强方法, 结果验证了我们数据集的有效性和数据增强方法的适用性.