信息来源： RUC明理新声 发布日期：2026年1月15日

在小说阅读器中沉浸阅读数字时代的科学与技术

2025

2025-2026学年秋季学期“数字时代的科学与技术”第十二讲由数学学院副教授王善文带来《人工智能与数学》主题讲座。

讲座从人工智能冲击国际数学奥林匹克（IMO）的现象切入，重点介绍了 DeepMind 的 Alpha-Geometry 和 AlphaProof 模型，详细阐述了选择平面几何作为首要冲击对象的原因（包括其自封闭的公理化系统、定理数量较少、门槛较低、受众广以及前期自动研究积累多），并现场利用 Alpha-Geometry 演示了 IMO 2000 年第一题的解题过程。

讲座系统梳理了人类研究数学的历史与“数学形式化”的概念，提及了从中国古代算筹到探索素数公式的数学历程。讲座定义了“数学形式化”为使用证明助手将自然语言转化为计算机程序的过程，并解释了进行形式化的目的在于实现数学的机械化、数字化和智能化。

讲座通过回顾数学形式化的发展阶段，描述了从早期的尝试，到数学界的“冷淡期”，再到“Hales 传奇”带来的转折与上升期，重点讲述了 2017 年 Kevin Buzzard 教授在伦敦帝国理工学院成立 Xena 项目（Lean 俱乐部），以及计算机界 Lean 社区邀请 Xena 共同建立数学图书馆（mathlib）的标志性事件。

讲座最后总结了数学形式化的深入发展与 ITP（交互式定理证明）及 AP（自动定理证明）的前景，指出越来越多的复杂数学概念（如代数几何中的概型 Scheme 等）正在被形式化，展示了人工智能与数学深度融合的未来趋势。