为推动数学与人工智能（AI）的交叉融合创新，拓展机器证明与智能算法在数学研究中的应用边界，2025年8月8日，在第十五届中国数学会计算机数学大会期间，哈尔滨师范大学特邀中国科学院数学与系统科学研究院陈绍示研究员，在哈尔滨理工大学作题为《机器证明与AI新技术及其应用》的专题科普报告。报告系统梳理并深入探讨了该交叉领域的前沿成果与发展方向，吸引了众多师生及科研工作者到场聆听。

陈绍示研究员首先回顾了机器证明的辉煌发展历程。从1950年图灵提出机器智能的构想，到1960年王浩利用计算机证明《数学原理》中的大量定理，再到1976年阿佩尔与哈肯借助计算机完成四色定理的证明，以及1978年吴文俊院士提出的革命性“吴方法”，实现了几何定理的机械化证明。他指出，这些里程碑式的成就不仅极大地推动了数学研究的自动化进程，也为软件验证、硬件安全等关键领域奠定了坚实基础。

报告中，陈绍示重点阐释了“吴方法”的核心思想与应用价值。该方法通过将几何问题转化为代数方程，并利用特定算法（如三角列与逐次除法）实现定理的自动证明。他通过开普勒定律推导、机器人路径规划等生动案例，展示了数学机械化的强大潜力与实际应用场景。

在介绍组合恒等式的机器证明时，陈绍示讲解了20世纪90年代Wilf与Zeilberger提出的WZ理论。他特别提到其团队在该领域的突破性贡献——解决了Wilf-Zeilberger猜想，并设计了自动化算法生成有理形式的WZ对。通过现场演示符号计算软件Maple证明具体恒等式，他直观展现了计算机在数学发现中不可替代的高效性与精确性。

符号计算作为机器证明的核心支撑技术，其重要性在报告中被多次强调。陈绍示详细介绍了符号计算涵盖的多项式运算、微分方程求解、代数几何等研究范畴，并展示了Maple软件在因数分解、符号积分等方面的强大功能。他指出，以Mathematica、Maple为代表的符号计算系统已成为现代数学研究不可或缺的工具，其算法的优化程度直接影响着复杂数学问题的求解效率。

展望未来，陈绍示研究员结合多个案例，指出“AI for Math (AI4Math)”是重要的发展方向，未来需深度融合人工智能技术与数学研究。他分享了多位数学家关于AI与数学融合的见解，强调了这种融合对数学学科未来发展产生的深远影响。

本次报告全面展示了AI与数学交叉领域的最新进展与广阔前景，为相关研究提供了重要参考。报告最后，与会教师与青年学者纷纷与陈绍示研究员进行互动学习，交流心得，现场气氛热烈，大家纷纷表示收获颇丰。陈绍示研究员同时勉励青年学者勇于探索这一充满活力的交叉领域，共同推动中国数学在人工智能时代的创新发展。