2025年3月31日，北京师范大学人工智能学院联合党委学生工作部在电子楼105成功举办京师智能讲堂第二十八期暨网络文化大讲堂活动。本次讲座邀请北京通用人工智能研究院王威研究员，以“人工智能在数学定理证明中的进展与挑战”为主题作报告，全校40余名学生积极参与本次活动。

王老师从数学定理证明的形式化描述切入，解析了自动定理证明的基本流程，包括自然语言的形式化转换、逻辑推理与证明过程自动生成。他指出，逻辑推理与直觉学习是解题(Problem Solving)的关键。此外，将自然语言问题转化为可推理的形式化表示，也是在实际应用中急需解决的一个问题。

王老师通过自主研发的代数推理引擎AIPS和智能几何系统TongGeometry，不仅能够大量生成题目，有些题目达到了国际奥林匹克数学竞赛（IMO）的难度水平，还能证明IMO级别的代数不等式和几何题，特别是在几何证明方面已经超过了谷歌Deepmind的AlphaGeometry系统。这两项技术的研发不仅推动了人工智能在几何和代数领域的应用，也为数学教育和竞赛提供了强有力的工具。

在交流环节，王威研究员进一步阐释了AI技术在数学定理证明与解题中的创新思路。他提出，未来需要进一步打造完备、易于使用的数学推理引擎，为学习提供高质量的数据支撑，使得其能够在更为广泛的数学领域发挥作用。此外，当前AI系统还属于“刷题”阶段，无法像人类一样，通过少数例子学会推理，未来应该聚焦模型抽象能力的研究与提升，使得其能够自己学习概念、提出定理，建立不同领域之间的关系，达到一流数学家的水平。

此次京师智能讲堂为师生们提供了学术交流的平台，人工智能学院将继续举办讲堂沙龙等学术活动，促进学生学业发展。