“宛如外星来客降临”：斯坦福FMS研讨会探讨人工智能对数学未来的深远影响
FMS（Future of Mathematics Symposium）“数学未来”研讨会，于2026年5月1日至2日在斯坦福大学举行。
图中人物：玛丽娜・维亚佐夫斯卡、陶哲轩。（摄影：Angikar Ghosal / 《斯坦福日报》）
作者：Angikar Ghosal（斯坦福日报记者）2026-5-6
译者：zzllrr小乐（数学科普公众号）2026-6-7
5月初，三位菲尔兹奖得主、来自 OpenAI 与 DeepMind 的研究人员，以及数十位数学家和计算机科学家齐聚斯坦福，共同展望人工智能将如何重塑数学。
在斯坦福经济政策研究所为期两天的主题演讲与小组讨论中，与会者达成了一个明确共识：人工智能工具已然改变数学研究的方式，但该领域最核心的难题 —— 如提出恰当概念、理解证明为何成立、判断哪些问题有价值 —— 依然属于人类。
这一主线贯穿了研讨会多场重磅报告。在题为《新的数学工作流》的主旨演讲中（详情参阅：2026.5数学未来研讨会系列——新的数学工作流 by 陶哲轩——斯坦福FMS），加州大学洛杉矶分校菲尔兹奖得主陶哲轩指出，数学界不应再纠结于 “AI 能否生成或验证证明”，而是要正视他所说的“激励缺口”，并提出“证明消化” 概念 —— 即精简、阐释证明，并将其与既有文献和未来方向连接的过程。
“衡量成功的真正标准，不在于证明是否被生成或验证，而在于有人能否就此开展讲座并回答提问。” 陶哲轩说，“成功的标尺，是我们所做的能否让人们更清晰、更有效地思考与理解数学。”
同样是菲尔兹奖得主的迈克尔・弗里德曼（详情参阅：2026.5数学未来研讨会系列——压缩即为建模数学的核心 by 迈克尔・弗里德曼——斯坦福FMS），从结构角度阐述了挑战：我们的目标是引导 AI 在输入组合空间中保持合理路径。他随后表示，若 AI 能对数学家关心但尚未理解的问题给出可验证的证明凭证，将是 “最迷人、最激动人心的事件之一…… 宛如外星来客降临”。
来自 OpenAI 的塞巴斯蒂安・布贝克（Sébastien Bubeck）介绍了 GPT 系列模型在概率、组合数学与优化问题上的解题能力。
“未来几年，我们或许可以把思考外包出去，但理解是无法外包的。你必须亲自去理解。” 他说。
多位演讲者聚焦形式化数学现状，即用机器可检验的语言书写证明。目前成果显著但发展不均。
2022年菲尔兹奖得主、瑞士洛桑联邦理工学院的玛丽娜・维亚佐夫斯卡的获奖证明，已于2026年2月通过数学家与 Math Inc. 公司自动形式化模型 Gauss（高斯） 的合作完成形式化验证。详见：
2026.5数学未来研讨会系列——球体堆积问题的形式化by 玛丽娜·维亚佐夫斯卡（Maryna Viazovska，2022年菲尔兹奖得主）——斯坦福FMS
AI与人类协作在数学领域迎来里程碑时刻 ——21世纪菲尔兹奖获奖证明首次完成形式化验证——IEEE Spectrum
“这在数学界与形式化数学圈引发了大量讨论。” 维亚佐夫斯卡说。
定理证明器Lean的联合创始人莱奥・德・莫拉（Leonardo de Moura）探讨了 AI 时代的机器检验数学。他强调，即便工具不断进步，人类引导依然不可或缺：“你有责任检查命题与定义是否准确表达了论文意图…… 这依然是人类的工作。”
伦敦帝国理工学院教授凯文・巴扎德（Kevin Buzzard）聚焦自动形式化，并指出一个更基础的障碍：AI处理证明的能力越来越强，但现有形式化库漏洞百出。“大量数学内容实际上缺失…… 我们大多数人并未真正参与数学形式化。” 他表示，因此防止AI错误形式化定义至关重要。
其他报告展示了AI系统在数学研究中的现有能力与局限。
Google DeepMind 的Thang Luong发布了数学研究智能体Aletheia，基于 Gemini Deep Think 构建，能用自然语言生成、验证与修正解题过程。
“我们真的希望对学界保持透明。外界有很多消息称 AI 已经征服数学，但我认为这种说法并不准确。” 他澄清道。
同样来自DeepMind、曾任斯坦福物理系研究员的亚当・布朗（Adam Brown），提出了衡量大模型表现的基准测试。他对模型未来改进表示乐观，这将来自 “算法进步 —— 我们能用同样的数据与算力完成多得多的任务”。
AI在数学中的应用已经改变了部分高校的运作方式。加州大学洛杉矶分校数学系 AI 负责人安德里亚・贝尔托齐（Andrea Bertozzi）展示了 AI 在应用数学中的案例，包括AI评分工具，以及该校参与美国国防高级研究计划局（DARPA）“指数级数学” 项目的工作 —— 该项目旨在开发能提出并证明有用抽象概念的AI 合著者。参阅：
加州大学洛杉矶分校（UCLA）团队获DARPA500万美元合同，研发用于促进数学的AI人工智能
“列车已经驶离站台，而学生们正是列车的驾驶者。” 贝尔托齐说。
本次研讨会由斯坦福大学塞格奥数学助理教授贾里德・杜格尔・利克曼（Jared Duker Lichtman）联合数学未来研究所（FMI）共同组织，由斯坦福以人为本 AI 研究院（HAI）与斯坦福智能系统实验室（SISL）联合主办，并得到文艺复兴慈善基金会、BroadRiver 资产管理公司、OpenAI 与 KeyBank 的支持。
与会学者包括诺贝尔奖得主、斯坦福经济学教授保罗・米尔格罗姆与吉多・因本斯（Guido Imbens），以及图灵奖得主、计算机科学教授帕特・汉拉汉（Patrick M. Hanrahan）。顶尖 AI 实验室与科技企业的员工、大批研究生也参与了会议，其中不乏大量来自加州大学伯克利分校的学子。
斯坦福大学数学系教授、现任美国数学会主席拉维・瓦基尔（Ravi Vakil）呼吁数学界 “持续参与讨论，保持对局势的了解”。“令人不安的是，社会上对此的讨论充斥着误解与过度的悲观主义。”
参考资料
https://stanforddaily.com/2026/05/06/future-of-mathematics-symposium-2026/
2026.5斯坦福FMS数学未来研讨会系列——开场欢迎致辞
全球已有550多名数学家签名支持2026《人工智能与数学莱顿宣言》数学界绝境自救历史性一刻：如何守住人类数学的千年根基
2026.5数学未来研讨会系列——菲尔兹圆桌讨论主题：价值体系——斯坦福FMS
2026.5数学未来研讨会系列——球体堆积问题的形式化by 玛丽娜·维亚佐夫斯卡（Maryna Viazovska，2022年菲尔兹奖得主）——斯坦福FMS
2026.5数学未来研讨会系列——新的数学工作流 by 陶哲轩——斯坦福FMS
2026.5数学未来研讨会系列——压缩即为建模数学的核心 by 迈克尔・弗里德曼——斯坦福FMS
2026.5斯坦福FMS数学未来研讨会系列——菲尔兹研究所的数学人工智能研究 by 迪尔德丽・哈斯凯尔Deirdre Haskell
小乐数学科普：2022国际数学家大会一小时报告《数学形式主义的兴起》Kevin Buzzard 演讲全文
小乐数学科普：专访ICM 2022国际数学家大会一小时报告者Kevin Buzzard：计算机可以成为数学家吗？——译自量子杂志
https://www.math.inc/sphere-packing
https://actu.epfl.ch/news/prof-viazovska-s-proofs-of-sphere-packing-formaliz/
https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/