# 人工智能进军数学领域：数学家们准备好迎接了吗？ 在洛杉矶盖蒂博物馆的藏品中，有一幅17世纪古希腊数学家欧几里得的肖像：衣衫褴褛、蓬头垢面，双手沾满污垢，举着他的几何学著作《几何原本》。两千多年来，欧几里得的著作一直是数学论证和推理的典范。 卡内基梅隆大学逻辑学家Jeremy A vigad说：「众所周知，欧几里得以近乎诗意的 [定义] 开始。然后，他在此基础上建立了当时的数学，使用基本概念、定义和先验定理，以这样一种方式证明事物，即每一步都 [清晰地遵循] 前一步。」A vigad博士补充说，有人抱怨欧几里得的一些「明显」步骤并不明显，但该系统仍然有效。 但到了20世纪，数学家不再愿意将数学建立在这种直观的几何基础上。相反，他们开发了正式的系统——精确的符号表示、机械规则。最终，这种形式化使得数学能够转化为计算机代码。 1976年，四色定理（该定理指出四种颜色足以填充地图，因此没有两个相邻区域具有相同的颜色）成为第一个借助计算强力证明的主要定理。 现在，数学家们正在努力应对最新的变革力量：人工智能。 ## 人工智能的预测与挑战 2019年，曾在谷歌工作、现就职于旧金山湾区一家初创企业的计算机科学家Christian Szegedy预测，计算机系统将在十年内赶上或超过人类最优秀数学家解决问题的能力。去年他将目标日期修改为2026年。 普林斯顿高等研究院数学家、2018年菲尔兹奖获得者Akshay Venkatesh目前对使用人工智能不感兴趣，但他热衷于谈论它。「我希望我的学生意识到他们所处的领域将会发生很大的变化，」他在去年的一次采访中说道。他最近补充道：「我并不反对深思熟虑和刻意地使用技术来支持我们人类的理解。但我坚信，注意我们使用它的方式是至关重要的。」 二月，A vigad博士参加了在加州大学洛杉矶分校纯粹与应用数学研究所举办的「机器辅助证明」研讨会。这次聚会吸引了数学家和计算机科学家的非典型组合。「这感觉很重要，」该大学数学家、2006年菲尔兹奖获得者、研讨会的主要组织者Terence Tao说。 Tao博士指出，直到最近几年，数学家们才开始担心人工智能的潜在威胁，无论是对数学美学还是对他们自己。他说，著名的社区成员现在正在提出这些问题并探索潜在的「打破禁忌」。一位引人注目的研讨会参与者坐在前排：一个名为「举手机器人」的梯形盒子，每当在线参与者提出问题时，它就会发出机械的低语并举起手。「如果机器人可爱且不具有威胁性，那就很有帮助，」Tao博士说。 > **小提示**：数学家们对AI的态度正在从“忽视”转向“主动探索”，这表明AI在数学领域的应用已经成为一个不可回避的趋势。 --- ## 带来「证明抱怨者」：证明助手工具 如今，优化我们生活的小工具并不缺乏——饮食、睡眠、锻炼。威斯康星大学麦迪逊分校数学家Jordan Ellenberg在研讨会休息期间说：「我们喜欢给自己附加一些东西，以便更容易把事情做好。」他补充说，人工智能设备可能也会对数学产生同样的影响。「很明显，问题是，机器能为我们做什么，而不是机器会对我们做什么。」 一种数学小工具称为证明助手，或交互式定理证明器。（「自动化」是20世纪60年代的早期化身。）数学家一步步将证明转化为代码；然后软件程序检查推理是否正确。验证积累在一个库中，这是其他人可以查阅的动态规范参考。霍斯金森形式数学中心（由加密货币企业家Charles Hoskinson资助）主任A vigad博士说，这种形式化为当今的数学奠定了基础，「就像欧几里得试图编纂和整理数学一样，为他那个时代的数学奠定了基础。」 ### 关注焦点：Lean证明辅助系统 最近，开源证明辅助系统Lean备受关注。Lean由现任职于亚马逊的计算机科学家Leonardo de Moura在微软开发，Lean使用自动推理，由所谓的老式人工智能 (GOFAI) 提供支持，即受逻辑启发的符号人工智能。到目前为止，Lean社区已经验证了一个关于将球体翻转的有趣定理，以及统一数学领域方案中的一个关键定理以及其他策略。 但证明助手也有缺点：它经常抱怨自己不理解数学家输入的定义、公理或推理步骤，因此它被称为「证明抱怨者」。所有这些抱怨会使研究变得麻烦。但是福特汉姆大学的数学家Heather Macbeth说，同样的功能（提供逐行反馈）也使该系统对教学很有用。 ### 教学中的应用案例 今年春天，Macbeth博士设计了一门「双语」课程：她把黑板上的每个问题都翻译成课堂讲稿上的Lean代码，学生们用Lean和散文两种语言提交作业问题的解决方案。「这给了他们信心，」Macbeth博士说，因为他们得到了即时的反馈，知道证明何时完成，以及过程中的每一步是对还是错。 参加研讨会后，约翰霍普金斯大学的数学家Emily Riehl使用了一个实验性的证明助理程序，将她之前与一位合著者发表的证明正式化。在一次验证结束时，她说，「我真的非常非常深入地理解了这个证明，比我以前理解的要深入得多。我想得很清楚，我可以向一台非常愚蠢的计算机解释。」 > **常见问题**：证明助手（如Lean）的主要缺点是什么？ > > **答案**：证明助手的主要缺点是它会频繁“抱怨”，即不理解数学家输入的定义、公理或推理步骤，这会导致研究过程变得繁琐。许多数学家将其形象地称为“证明抱怨者”。不过，这种逐行反馈功能在教学环境中反而成为优势，帮助学生即时验证推理过程的正确性。 --- ## 蛮力推理——但它是数学吗？ 卡内基梅隆大学计算机科学家、亚马逊学者Marijn Heule使用的另一种自动推理工具是他俗称的「暴力推理」（brute reasoning）。他说，只要用精心设计的编码来说明你想要找到哪个「奇异物体」，超级计算机网络就会在搜索空间中进行搅动，并确定该实体是否存在。 就在研讨会之前，Heule博士和他的一位博士学生Bernardo Subercaseaux最终解决了一个长期存在的50 TB文件问题的解决方案。然而，该文件与Heule博士及其合作者在2016年得出的结果几乎没有可比性：「200 TB的数学证明是有史以来最大的」，《Nature》杂志的一个标题宣布。文章接着问，用这些工具解决问题是否真的算作数学。在Heule博士看来，这种方法是「解决人类无法解决的问题」所必需的。 > **小提示**：暴力推理虽然能解决人类无法解决的问题，但其生成的证明文件往往巨大（如200TB），这让许多传统数学家质疑其是否“真正算作数学”。 ### 机器学习工具的登场 另一组工具使用机器学习，它可以合成大量数据并检测模式，但不擅长逻辑、逐步推理。谷歌的DeepMind设计了机器学习算法来解决蛋白质折叠 (AlphaFold) 和国际象棋获胜 (AlphaZero) 等问题。在2021年《Nature》杂志的一篇论文中，一个团队将他们的成果描述为「通过人工智能指导人类直觉来推进数学发展」。 前谷歌计算机科学家、现在在湾区创业的Yuhuai「Tony」Wu概述了一个更宏伟的机器学习目标：「解决数学问题」。在谷歌，Wu博士探索了支持聊天机器人的大型语言模型如何帮助数学。该团队使用的模型经过互联网数据训练，然后使用数学和科学论文的在线存档等富含数学的大型数据集进行微调。Wu博士在研讨会上说，当用日常英语要求解决数学问题时，这个名为Minerva的专门聊天机器人「非常擅长模仿人类」。该模型在高中数学考试中获得的成绩优于16岁学生的平均成绩。 Wu博士说，最终，他设想了一位「自动化数学家」，具有「自行解决数学定理的能力」。 > **常见问题**：机器学习工具与证明助手（如Lean）在数学领域的主要区别是什么？ > > **答案**：证明助手（如Lean）依赖于符号逻辑和自动推理（GOFAI），通过逐步检查数学证明的正确性来工作，擅长严格推理。而机器学习工具（如DeepMind的模型或Minerva）通过分析大量数据检测模式，擅长直觉式问题解决，但在逻辑逐步推理方面较弱。两者互补但各有局限。 --- ## 数学作为试金石：AI的局限与伦理思考 数学家们对这些干扰做出了不同程度的关注。 哥伦比亚大学的Michael Harris在他的「Silicon Reckoner」子堆栈中表达了疑虑。他对研究数学与科技和国防工业之间潜在的冲突目标和价值观感到困扰。 Harris博士对缺乏对人工智能更大影响的讨论表示遗憾。数学研究，特别是「与正在进行的非常活跃的对话相比」，「除了数学之外，几乎无处不在」。 DeepMind合作者、悉尼大学的Geordie Williamson在N.A.S.发表了讲话，鼓励数学家和计算机科学家更多地参与此类对话。在洛杉矶的研讨会上，他以改编自乔治·奥威尔1945年文章「You and the Atom Bomb」的一句话开始了自己的演讲。Williamson博士说：「考虑到我们所有人在未来五年内都可能受到深刻影响，深度学习并没有引起像预期的那样多的讨论。」 Williamson博士认为数学是机器学习能做什么或不能做什么的试金石。推理是数学过程的精髓，也是机器学习中尚未解决的关键问题。 ### 黑匣子里的直觉 Williamson博士在接受采访时表示，在与DeepMind合作的早期，该团队发现了一个简单的神经网络，它可以预测「我非常关心的数学量」，而且它的预测「准确得可笑」。Williamson博士努力想要理解其中的原因——这将成为一个定理的基础——但是却无法理解。DeepMind的任何人都做不到。就像古代几何学家欧几里得一样，神经网络以某种方式直观地辨别出了数学真理，但其逻辑「原因」却远非显而易见。 在洛杉矶研讨会上，一个突出的主题是如何将直觉和逻辑结合起来。如果人工智能能同时做到这两件事，一切都将迎刃而解。 但是，Williamson博士观察到，人们很少有动力去理解机器学习所呈现的黑匣子。他说：「这是科技界的黑客文化，如果它在大部分时间都有效，那就太好了。」但这种情况让数学家们感到不满。 他补充说，试图理解神经网络内部发生的事情会引发「令人着迷的数学问题」，而寻找答案为数学家「为世界做出有意义的贡献」提供了机会。 > **常见问题**：为什么数学家对机器学习模型的“黑匣子”感到不满？ > > **答案**：因为机器学习模型可以做出高度准确的预测（如预测数学量），但人们无法理解其内部逻辑和推理过程。数学家希望理解事物背后的“为什么”以形成严谨的定理证明，而“黑匣子”仅提供结果却不解释原因，这与数学追求的“严密逻辑推导”精神相悖。 --- ## 总结与展望 随着2026年的临近，Christian Szegedy的预言能否实现仍是一个开放问题。但可以肯定的是，人工智能已经以三种主要形式进入了数学领域： 1. **证明助手（如Lean）**：通过逻辑符号和自动推理验证证明的正确性 2. **暴力推理（如Marijn Heule的工作）**：通过超级计算机搜索空间寻找解 3. **机器学习（如Minerva、DeepMind）**：通过数据学习模式，提供直觉性预测 未来，数学家面临的挑战不仅是技术层面，更是哲学层面——如何在机器辅助下保持数学的严谨性和美学价值，同时利用AI解决那些人类无法单独解决的问题。正如Williamson博士所说，理解神经网络内部机制本身就是一个「令人着迷的数学问题」，可能是未来数学家的重要工作方向之一。