两位计算机数学专家应邀为我院师生作学术报告

2025年6月9日下午，中国科学院数学与系统科学研究院冯如勇研究员、华东师范大学杨争峰教授应邀来访我院，并于203报告厅分别作了题为《Stable D-finite Functions Under Integration》和《面向组合数学的定理自动生成和证明》的学术报告。

冯如勇教授首先回顾了数学中经典的“有限项积分”问题，并指出传统方法（如Liouville定理和Risch算法）的局限性。接着介绍了团队在D-有限函数的稳定性理论领域取得的成果，为解决微分方程与符号积分中的关键问题提供了新的理论工具和算法支持。最后，研究团队未来计划将理论扩展至高阶微分算子，并探索其在人工智能、符号推理和数学机械化证明中的应用。

杨争峰教授首先回顾了计算机在数学证明中的里程碑应用，如四色猜想和开普勒猜想的计算机辅助证明，并指出近年来AI技术（如DeepMind的AlphaTensor、AlphaGeometry和AlphaProof）在解决复杂数学问题上的卓越表现。接着介绍了其团队结合AI大语言模型和强化学习理论，开发了一个基于Lean的组合恒等式形式化数据集LeanComb，及其相应的定理自动证明器，针对组合恒等式的问题，其证明准确率上优于现有的证明器。最后，指出了当前仍面临数据稀缺性、大语言模型可靠性等挑战。

冯如勇，中国科学院数学与系统科学研究院研究员，2005年在中国科学院数学与系统科学研究院获得博士学位。主要研究方向为：符号计算，微分/差分代数，发展了非线性自治微分差分方程的符号求解算法，改进了Hrushovski计算微分伽罗瓦群的算法、证明了关于绝对微分伽罗瓦群的Matzat猜想，并开发了计算差分伽罗瓦群的算法。于2010年获得中科院系统科学研究所关肇直青年研究奖、2014年获得中科院数学与系统科学研究院突出科研成果奖，2017年获得首届吴文俊计算机数学青年学者奖，2021年获得国际符号与代数计算年会最佳论文奖。

杨争峰，华东师范大学软件工程学院教授。于2006年获得中国科学院数学与系统科学研究院博士学位。主要研究方向为数学机械化、人工智能数学、混成系统验证等。迄今为止在CAV、FM、ISSAC、NeurIPS、CVPR、EMSOFT等国际会议和ACM TECS、IEEE TCAD、JSC等国际期刊上发表了80余篇论文。近年来主持国家重点研发计划“数学和应用研究”专项课题、国防科工委创新项目、国家自然科学基金等多个科研课题。

（审核人：彭江涛）