本研究针对大型语言模型在组合恒等式自动定理证明中的训练数据不足问题，构建了LeanComb基准并开发了自动定理生成器ATG4CI，生成了260K组合恒等式数据集。研究结果表明，基于该数据集训练的模型在自动定理证明中的成功率显著提高。