当 AI 能做数学时，成为数学家意味着什么
2000 年代中期，当我路过的每间酒吧和夜店都放着 Killers 和 Franz Ferdinand 的音乐时，我正日以继夜地攻读应用数学博士学位。我的研究专注于模拟特殊光波在液晶中的相互作用，并用简单方程来近似和理解这些相互作用。如今回头看我的论文，液晶技术早已过时，我估摸我的工作若借助 AI 辅助，几天——甚至几小时——就能完成。
但与我共享爱丁堡大学那间拥挤办公室的纯数学博士生们的情况，就完全不同了。当时我为这些同事感到惋惜，他们日复一日坐在桌前，仿佛在抓耳挠腮却毫无进展。（虽然我自己也在挣扎，但至少总能有些进展。）当我们毕业各奔东西时，有些人甚至一篇论文都没发表。
如今回想起来，我终于明白他们为何会花数年时间钻研那些全世界只有少数人在意的抽象数学问题。那并非我当时以为的傲慢——他们并非试图通过率先解决某个看似棘手的数学问题来证明自己的超群智力。那甚至也不是某种受虐倾向（这是我的第二个猜测）——并非为想象中的不足而赎罪。我意识到，他们从通向理解的漫长旅途中获得了喜悦、满足和意义。
"有时候，理解就这样击中了你，你觉得它非常美。"
——卡内基梅隆大学，Jeremy Avigad
"有时候，理解就这样击中了你，你觉得它非常美。有时它是一种成就感，就像跑完一场马拉松，"卡内基梅隆大学的数学家 Jeremy Avigad 若有所思地说。"但它又不完全是这两种感觉：当你对一个复杂而困难的问题长时间深入思考，然后——突然间——一切就串联起来了，那是一种美妙的感觉。"
这种感觉贯穿了数学史的始终。同样，数学家追求这种感觉的方式几个世纪以来也几乎没有变化。他们观察或想象数字、形状或逻辑结构中的联系、模式或性质。在此基础上，他们写下猜想——对其推测的未经验证的陈述。然后他们或其他数学家运用逻辑推理和数学工具，以富有创造力的方式证明或证伪这些猜想。最后，又由其他数学家来验证（或质疑）这些证明。
这个过程不可避免地需要大量的思考时间。"我去参加了一个纯数学夏令营，上课时我们会花半小时面对一道难题，没人说话——每个人都在思考，"佛蒙特大学的数学家兼计算机科学家 Krystal Maughan 说（她即将获得博士学位）。"但随后我们会一起协作，一步步解构这个问题。"
这就是数学那历久弥新的乐趣。但如今的 AI 系统正开始切入并绕过这一缓慢的深思过程。沿着这个趋势推演到极致：如果 AI 让数学家的挣扎变得完全多余会怎样？AI 是否甚至可能将人类彻底边缘化？
AI 对数学的渗透：从四色定理到菲尔兹奖级成果
几十年来，计算技术一直在加速数学进步。这始于 50 年前，当时数学家使用计算机证明了四色定理——该定理问的是：是否任何地图都可以用不超过四种颜色着色，使得相邻区域颜色不同？答案是肯定的，而计算机通过检查 1,936 种情况证明了它，这种方式人类根本无法实际验证，在当时引发了巨大争议。
然而在整个计算时代，即使是在依赖海量计算资源的证明中，人类数学家的角色始终处于核心地位。人类凭借直觉提出猜想，凭借创造力和经验设计证明策略，然后人类来验证这些证明是否正确。
如今 AI 正在挑战这一格局。短短几年间，大语言模型（LLM）已从"随机鹦鹉"——只能复述从互联网抓取的基本数学知识——进化成了高级数学推理机器。
去年夏天，Google DeepMind 和 OpenAI 的系统达到了相当于全球最具数学天赋高中生的水平，在国际数学奥林匹克竞赛中斩获金牌。在这项年度赛事中，参赛者必须解决六道来自数学各领域的著名难题。
今年早些时候，Google DeepMind 的实验性 AI 系统 Aletheia 实现了更重要的里程碑：它自主产出了可发表的博士级研究成果。虽然该成果本身在数学上较为冷门——在算术几何中计算结构常数——但其意义在于它在攻克一个未解决的数学问题时所展现的复杂推理能力。更近期，OpenAI 的一个新型通用 AI 系统推翻了组合几何中的一个重要猜想。如果该成果由人类完成，完全有资格发表在顶级数学期刊上，顶尖数学家们盛赞这是 AI 在数学领域的一座里程碑，展示了独立、原创且精深的思维能力。
另一个转变来自 LLM 与被称为"证明助手"的数学工具的结合，这类工具已存在十多年。这些系统——如 Isabelle、Lean 和 Rocq——是专门的编程语言，能够逐步检查数学证明并验证其逻辑正确性。传统上，数学家必须手动将定理和证明翻译成这种机器可读的格式，这是一项名为"形式化"的繁重工作。现在，LLM 正开始消除这一瓶颈，自动将非形式化的证明翻译成证明助手可验证的形式化代码。
上图展示了欧几里得关于素数无限性的著名证明在 Lean 证明助手中形式化后的样子。人类数学家通常跳过步骤并依赖共同理解；形式化则让每一个假设和推理都显式化，以便计算机验证证明。
这类系统（有时被称为推理代理）已变得高度精密。今年 2 月，AI 公司 Math, Inc. 使用了它那个野心勃勃的推理代理 Gauss，将数学家 Maryna Viazovska（瑞士洛桑联邦理工学院）2022 年获得菲尔兹奖的证明进行了形式化。Gauss 首先帮助人类数学家数天内完成了 Viazovska 八维球体堆积问题解的形式化，随后自主地在两周内完成了更复杂的 24 维情况的形式化。
这些成就表明，AI 已能够处理一些长期被认为是人类专属的数学任务。随着技术不断进步，人类数学家越来越多的日常工作可能被 AI 染指。
人类数学家可能变成"神谕的祭司"。
——伦敦数学科学研究所，Yang-Hui He
海德堡论坛上的存在主义焦虑
2025 年 9 月，我参加了第 12 届海德堡桂冠论坛——这是一场年度会议，将数百名年轻的数学家和计算机科学家与他们的学术偶像聚集在一起。AI 主导了所有讨论，从一开始，空气中就弥漫着紧张感。
演讲者描绘了一个未来：超人类 AI 数学家超越了人类的知识和能力——提出猜想、搜索解空间、证明猜想，最后验证证明并推广结果，全程无需人类参与。如果这个未来成真，伦敦数学科学研究所的 Yang-Hui He 令人难忘地宣称，人类数学家可能变成"神谕的祭司"。
当这样惊人的预言在台上被提及时，我的目光投向了观众席。皱眉、坐立不安、交换眼神——人群的不安显而易见。澳大利亚迪肯大学的学生 Trill White 后来回忆说，坐在那个大厅里时她想着："'这太令人沮丧了。人类还能为数学贡献什么？数学会变成没人能理解的东西吗？'我确实感觉到，这将改变一切。"
"我们当然开始意识到 AI 有潜力取代我们。"Google Developer Groups 的南非数学家 Jessica Randall 说。她察觉到年轻数学家中弥漫着一种集体性的存在主义恐惧。"我能感觉到每个人都很担忧，因为他们还没想过那么远，"她说。"就像一颗重磅炸弹击中我们，我们当然开始意识到 AI 有潜力取代我们。"
一些知名数学家，包括 He 在内，似乎对 AI 接手目前属于人类数学家的工作感到坦然。那是因为他们只想知道数学中最重大问题的答案——比如六个尚未解决的千禧年大奖难题——即使这一切都由 AI 完成。"很多数学家都很务实，他们只想要理解。他们愿意为问题的解出卖灵魂，"Avigad 开玩笑说。"不惜一切代价，对吧？"
但这个"只想知道"阵营远非唯一的声音：大多数数学家并不希望或期待 AI 完全取代他们。相反，两种更广泛的替代路线正在浮现。第一种是以人类为中心的愿景，将人类对数学的理解放在首位，将 AI 仅视为工具（就像计算器一样）。第二种是协作式的"团队合作让梦想成真"愿景，人类和 AI 协同攻克任何一方都无法独立解决的问题。
数字"是一种让我们达成一致的方式"。
——普林斯顿大学，Akshay Venkatesh（菲尔兹奖得主）
两种愿景：人本主义 vs. 人机协作
菲尔兹奖得主、普林斯顿大学的数学家 Akshay Venkatesh 多年来一直在从人本主义视角思考这个问题。2022 年，他利用自己的菲尔兹奖研讨会恳请数学界深入思考 AI 对数学实践可能意味着什么。当时，AI 取代数学家的想法似乎还很遥远。现在他说："我们正在接近这样一个临界点：至少在部分抽象数学推理任务中，计算机正变得与人类具有竞争力。"
对 Venkatesh 而言，问题不仅在于计算机能做什么，还在于数学本身的目的。"有时我觉得，当我们使用数字时，与其说我们在描述本质上属于数字的现象，不如说我们都能完全同意这些数字的含义，"他说。"这是一种让我们达成一致的方式。"
渥太华大学的 Maia Fraser 认为，数学不仅仅是寻找答案。对她来说，为理解一个问题而挣扎本身就是这门学科最大的回报之一。她表示，她从数学中获得的愉悦是某种独特的人类体验，整合了潜意识和意识思维。她描述了自己如何从直觉上感到某件事应该成立，然后逐渐推导出可以用严谨证明表达的东西。交流和分享这些深层次思考的产物是"一种集体智慧的形式，是人类精神中美好的东西"。
基于这些论点，一个长期困扰人类的数学猜想即使被 AI 证明了，也只有当人类能够理解时才有意义。"AI 能证明这个陈述已经是有用的信息了，"Fraser 承认。"但提出一个优雅、优美的人类证明仍然是一个未解决的问题。"即使不存在这样的人类证明，寻找它的过程"仍然是一项有价值的努力"。
来自 Terence Tao 的是一种更具协作性的 AI 数学方法。Tao 在 10 岁时首次参加数学奥林匹克竞赛。1986 年、1987 年和 1988 年，他分别获得了铜牌、银牌和金牌，成为奥林匹克历史上最年轻的奖牌得主。如今，作为菲尔兹奖得主和加州大学洛杉矶分校教授，他赢得了在世最具天赋数学家之一的声誉。
与他的一些同行不同，Tao 既不排斥 AI，也不畏惧它。相反，他将 AI 视为学科根本性转变的催化剂——一种向他所称的"大数学"的转型。他设想了一个人机之间大规模、去中心化协作的未来，复杂的数学任务可以被拆分切分，人类占据创造性部分，而 AI 承担大部分技术性体力活。
Tao 已经在实验这一概念，与众多在线协作者一起解题，其中一些人使用 AI 工具。"一百年前，几乎每篇数学论文都是单独作者，"他说。"但现在我与素未谋面的人合作——未来，我可能都不知道对方是 AI 还是真人。"
Tao 愿景的关键是数学特有的：形式化。当一个证明被翻译成代码并由证明助手逐步检查时，就消除了任何人为错误或不诚实的可能。这种方法改变了协作的方式，因为信任是通过验证而非声誉或关系建立的。一个来自无名研究者甚至业余爱好者的想法，只要它有形式化证明，就可以被认真对待。
"如果不是因为这个形式化验证层，不设任何保障地开放项目将是一场灾难，"Tao 补充道。"但在数学中，我们可以完全检查和验证输出，这确实过滤掉了大量垃圾。"
未来的隐忧：精英化、动机丧失与智力萎缩
从海德堡桂冠论坛的年轻研究者到该领域的一些最响亮的名字，数学家们似乎在一个问题上达成了一致：AI 有潜力改变他们的学科。但这种变革在实践中意味着什么，共识则少得多。
一些人担心 AI 工具的可及性。传统上，数学家推进其领域所需要的不过是直觉、训练以及纸和笔。如果这种缓慢、深思熟虑的过程不再被社会——尤其是研究资助方——所重视，那么数学可能变成一种精英活动，只有那些能够负担专有 AI 模型的特定组织才能参与。
另一个担忧是动机。随着 AI 系统承担越来越多的工作，深入钻研难题的动力可能会减弱。普林斯顿大学的 Venkatesh 表示，人类长期构建和理解一个证明的过程可能难以向资助方——甚至向数学家自己——证明其合理性。"有些时候，我花了数年时间思考某个问题，慢慢地挣扎着去理解它，"他说。"如果你的计算机能为你完成其中大部分工作，你还有动力去花那么多时间吗？"
这种担忧延伸到下一代。如果学生可以用 AI 直接跳到答案，他们很可能会这么做。但每一次跳过挣扎，他们就错过了一次建立自己独特直觉基础的机会。有人担心，长此以往，下一代数学家可能会遭受某种形式的"智力萎缩"，无法在训练他们的 AI 框架之外思考。
面对这些担忧，数学界正在采取行动。个人在撰写文章、组织研讨会、在期刊上辩论，而机构和社区团体正在制定关于如何在研究和出版中使用 AI 的指南。事实上，数学家们正在运用他们日常使用的同样严谨和好奇心，来应对 AI 带来的挑战。这些努力共同反映了数学界试图在 AI 时代保留对数学方向控制权的广泛尝试。
那么，AI 是否在榨干数学的灵魂？从某种意义上说，恰恰相反。它正在迫使数学家面对深刻的问题：数学是什么，他们为何将一生献给它，以及数学在社会中扮演着什么角色。与此同时，它也在以一种可能难以逆转的方式重塑数学的实践。
"数学让我成为更好的普通问题解决者，因为它训练我的思维以非常逻辑、理性的方式思考，"Randall 说，她正是在海德堡论坛上感受到存在主义恐惧的人之一。"它帮助我生活的方方面面。"随着 AI 改变数学，许多研究者想知道未来的数学家是否还能说出同样的话。
Benjamin Skuse 是一名专业的自由科技撰稿人。此前，他在爱丁堡大学获得了应用数学博士学位，并在西英格兰大学获得了科学传播硕士学位。他的作品曾发表于 New Scientist、WIRED、Physics World、Sky & Telescope、Photonics Focus 等众多媒体。
原文：AI in Mathematics Is Forcing Big Questions — IEEE Spectrum
