人工智能进军数学领域，数学家们准备好迎接了吗？

在洛杉矶盖蒂博物馆的藏品中，有一幅17世纪古希腊数学家欧几里得的肖像：衣衫褴褛、蓬头垢面，双手沾满污垢，举着他的几何学著作《几何原本》。

两千多年来，欧几里得的著作一直是数学论证和推理的典范。

卡内基梅隆大学逻辑学家Jeremy Avigad说：「众所周知，欧几里得以近乎诗意的 [定义] 开始。然后，他在此基础上建立了当时的数学，使用基本概念、定义和先验定理，以这样一种方式证明事物，即每一步都 [清晰地遵循] 前一步。」

Avigad博士说，有人抱怨欧几里得的一些「明显」步骤并不明显，但该系统仍然有效。

但到了20世纪，数学家不再愿意将数学建立在这种直观的几何基础上。相反，他们开发了正式的系统——精确的符号表示、机械规则。最终，这种形式化使得数学能够转化为计算机代码。

1976年，四色定理（该定理指出四种颜色足以填充地图，因此没有两个相邻区域具有相同的颜色）成为第一个借助计算强力证明的主要定理。

现在，数学家们正在努力应对最新的变革力量：人工智能。

2019年，曾在谷歌工作、现就职于旧金山湾区一家初创企业的计算机科学家Christian Szegedy预测，计算机系统将在十年内赶上或超过人类最优秀数学家解决问题的能力。去年他将目标日期修改为2026年。

普林斯顿高等研究院数学家、2018年菲尔兹奖获得者Akshay Venkatesh目前对使用人工智能不感兴趣，但他热衷于谈论它。「我希望我的学生意识到他们所处的领域将会发生很大的变化，」他在去年的一次采访中说道。他最近补充道：「我并不反对深思熟虑和刻意地使用技术来支持我们人类的理解。但我坚信，注意我们使用它的方式是至关重要的。」

二月，Avigad博士参加了在加州大学洛杉矶分校纯粹与应用数学研究所举办的「机器辅助证明」研讨会。这次聚会吸引了数学家和计算机科学家的非典型组合。「这感觉很重要，」该大学数学家、2006年菲尔兹奖获得者、研讨会的主要组织者Terence Tao说。

Tao博士指出，直到最近几年，数学家们才开始担心人工智能的潜在威胁，无论是对数学美学还是对他们自己。他说，著名的社区成员现在正在提出这些问题并探索潜在的「打破禁忌」。一位引人注目的研讨会参与者坐在前排：一个名为「举手机器人」的梯形盒子，每当在线参与者提出问题时，它就会发出机械的低语并举起手。「如果机器人可爱且不具有威胁性，那就很有帮助，」Tao博士说。

带来「证明抱怨者」

如今，优化我们生活的小工具并不缺乏——饮食、睡眠、锻炼。威斯康星大学麦迪逊分校数学家Jordan Ellenberg在研讨会休息期间说：「我们喜欢给自己附加一些东西，以便更容易把事情做好。」 他补充说，人工智能设备可能也会对数学产生同样的影响。「很明显，问题是，机器能为我们做什么，而不是机器会对我们做什么。」

一种数学小工具称为证明助手，或交互式定理证明器。（「自动化」是20世纪60年代的早期化身。）数学家一步步将证明转化为代码；然后软件程序检查推理是否正确。验证积累在一个库中，这是其他人可以查阅的动态规范参考。霍斯金森形式数学中心（由加密货币企业家Charles Hoskinson资助）主任 Avigad 博士说，这种形式化为当今的数学奠定了基础，「就像欧几里得试图编纂和整理数学一样。为他那个时代的数学奠定了基础。」

最近，开源证明辅助系统Lean备受关注。Lean由现任职于亚马逊的计算机科学家Leonardo de Moura在微软开发，Lean使用自动推理，由所谓的老式人工智能 (GOFAI) 提供支持，即受逻辑启发的符号人工智能。到目前为止，Lean社区已经验证了一个关于将球体翻转的有趣定理，以及统一数学领域方案中的一个关键定理以及其他策略。

但证明助手也有缺点：它经常抱怨自己不理解数学家输入的定义、公理或推理步骤，因此它被称为「证明抱怨者」。所有这些抱怨会使研究变得麻烦。但是福特汉姆大学的数学家Heather Macbeth说，同样的功能（提供逐行反馈）也使该系统对教学很有用。

今年春天，Macbeth博士设计了一门「双语」课程：她把黑板上的每个问题都翻译成课堂讲稿上的Lean代码，学生们用Lean和散文两种语言提交作业问题的解决方案。「这给了他们信心，」Macbeth博士说，因为他们得到了即时的反馈，知道证明何时完成，以及过程中的每一步是对还是错。

参加研讨会后，约翰霍普金斯大学的数学家Emily Riehl使用了一个实验性的证明助理程序，将她之前与一位合著者发表的证明正式化。在一次验证结束时，她说，「我真的非常非常深入地理解了这个证明，比我以前理解的要深入得多。我想得很清楚，我可以向一台非常愚蠢的计算机解释。」

蛮力推理——但它是数学吗？

卡内基梅隆大学计算机科学家、亚马逊学者Marijn Heule使用的另一种自动推理工具是他俗称的「暴力推理」（brute reasoning）。他说，只要用精心设计的编码来说明你想要找到哪个「奇异物体」，超级计算机网络就会在搜索空间中进行搅动，并确定该实体是否存在。

就在研讨会之前，Heule博士和他的一位博士。学生Bernardo Subercaseaux最终解决了一个长期存在的50 TB文件问题的解决方案。然而，该文件与 Heule 博士及其合作者在2016年得出的结果几乎没有可比性：「200 TB的数学证明是有史以来最大的」，《Nature》杂志的一个标题宣布。文章接着问，用这些工具解决问题是否真的算作数学。在Heule博士看来，这种方法是「解决人类无法解决的问题」所必需的。

另一组工具使用机器学习，它可以合成大量数据并检测模式，但不擅长逻辑、逐步推理。谷歌的DeepMind设计了机器学习算法来解决蛋白质折叠 (AlphaFold) 和国际象棋获胜 (AlphaZero) 等问题。在2021年《Nature》杂志的一篇论文中，一个团队将他们的成果描述为「通过人工智能指导人类直觉来推进数学发展」。

前谷歌计算机科学家、现在在湾区创业的Yuhuai 「Tony」 Wu概述了一个更宏伟的机器学习目标：「解决数学问题」。在谷歌，Wu博士探索了支持聊天机器人的大型语言模型如何帮助数学。该团队使用的模型经过互联网数据训练，然后使用数学和科学论文的在线存档等富含数学的大型数据集进行微调。Wu博士在研讨会上说，当用日常英语要求解决数学问题时，这个名为Minerva的专门聊天机器人「非常擅长模仿人类」。该模型在高中数学考试中获得的成绩优于16岁学生的平均成绩。

Wu博士说，最终，他设想了一位「自动化数学家」，具有「自行解决数学定理的能力」。

数学作为试金石

数学家们对这些干扰做出了不同程度的关注。

哥伦比亚大学的Michael Harris在他的「Silicon Reckoner」子堆栈中表达了疑虑。他对研究数学与科技和国防工业之间潜在的冲突目标和价值观感到困扰。

Harris博士对缺乏对人工智能更大影响的讨论表示遗憾。数学研究，特别是「与正在进行的非常活跃的对话相比」，「除了数学之外，几乎无处不在」。

DeepMind合作者、悉尼大学的Geordie Williamson在N.A.S. 发表了讲话。聚集并鼓励数学家和计算机科学家更多地参与此类对话。在洛杉矶的研讨会上，他以改编自乔治·奥威尔1945年文章「You and the Atom Bomb」的一句话开始了自己的演讲。Williamson博士说：「考虑到我们所有人在未来五年内都可能受到深刻影响，深度学习并没有引起像预期的那样多的讨论。」

Williamson博士认为数学是机器学习能做什么或不能做什么的试金石。推理是数学过程的精髓，也是机器学习中尚未解决的关键问题。

Williamson博士在接受采访时表示，在与DeepMind合作的早期，该团队发现了一个简单的神经网络，它可以预测「我非常关心的数学量」，而且它的预测「准确得可笑」。Williamson博士努力想要理解其中的原因——这将成为一个定理的基础——但是却无法理解。DeepMind的任何人都做不到。就像古代几何学家欧几里得一样，神经网络以某种方式直观地辨别出了数学真理，但其逻辑「原因」却远非显而易见。

在洛杉矶研讨会上，一个突出的主题是如何将直觉和逻辑结合起来。如果人工智能能同时做到这两件事，一切都将迎刃而解。

但是，Williamson博士观察到，人们很少有动力去理解机器学习所呈现的黑匣子。他说：「这是科技界的黑客文化，如果它在大部分时间都有效，那就太好了。」但这种情况让数学家们感到不满。

他补充说，试图理解神经网络内部发生的事情会引发「令人着迷的数学问题」，而寻找答案为数学家「为世界做出有意义的贡献」提供了机会。