本报告主要介绍了，自动化定理证明（ATP）传统上依赖于证明搜索，近年来，随着大语言模型的快速发展，AI赋能的定理自动证明已成为一种新范式。然而，由于现有证明数据的匮乏，基于人工智能的定理自动证明仍面临诸多挑战。针对组合恒等式定理自动证明问题，提出了一种融合大语言模型与强化学习的定理自动生成框架，通过融合人工形式化与定理自动生成方法，构建了一个基于Lean的组合恒等式形式化数据集，提升了模型的自动证明的效率和准确率；设计了LLM与符号计算融合的证明框架，将LLM的策略预测与经典的Wilf-Zeilberger（WZ）方法相结合，解决了此前单一方法难以处理的复杂恒等式证明问题。