报告摘要：

机器证明是数学与计算机科学的交叉领域。20世纪70年代，吴文俊院士在几何定理机器证明方面做出了先驱性工作。与几何定理证明一样，组合恒等式的传统证明方法往往具有高度的技巧性，没有统一性。20世纪90年代，组合学家Wilf和Zeilberger发展了组合恒等式机器证明的算法理论，即WZ理论。该理论彻底改变了组合恒等式与特殊函数论的研究面貌,并成为符号计算应用于组合数学、数论、数学物理等领域的桥梁。本报告将介绍WZ理论的基本算法、最新进展、以及在组合中的一些重要应用。

个人简介：

陈绍示，现为中国科学院数学与系统科学研究院研究员。主要研究符号计算与机器证明。在符号计算旗舰会议 ISSAC 与数学期刊 Algebra and Number Theory, Selecta Mathematica等发表论文40余篇。目前担任Journal of Symbolic Computation, Annals of Combinatorics, Journal of Difference Equations and Applications, Journal of Systems Science and Complexity, 和《系统科学与数学》等杂志编委，还担任国际符号与代数计算专业委员会秘书长与中国数学会计算机数学专业委员会秘书长. 曾获得第二届 “吴文俊计算机数学青年学者奖”(2019)，第46届国际符号与代数计算年会(ISSAC2021)“杰出论文奖”，与国际计算机代数应用大会(ACA2022)“青年学者奖”。2022年入选中国科学院青年创新促进会优秀会员。