AI赋能数学：智能助手如何改变我们的数学研究

研究者用ChatGPT证明数学定理，3年内AI会赶超数学家？

近年来，数学界越来越多的研究者开始关注人工智能对数学领域的潜在影响，并在各类研讨会中就这一主题展开辩论，同时积极尝试运用各种AI工具来解决数学问题。

数学作为机器学习的基石，其强大的能力在很大程度上决定了机器学习的发展方向和应用范围。推理作为数学的核心环节，更是机器学习中亟待攻克的难题。尽管神经网络在某种程度上直观地揭示了数学原理，但其背后的逻辑原因却并不十分明确。

加州理工学院和麻省理工学院研究者发布用大语言模型证明数学定理的论文。

最近一段时间，人工智能似乎在数学领域取得了进展，尽管一开始大语言模型被看作并不是特别适合数学推理。

上周，我国知名数学家、英伟达AI实验室数学家Jim Fan，转发了一篇来自加州理工学院与麻省理工学院的论文，该论文利用ChatGPT技术成功证明了数学定理，这标志着数学的AI助手（Copilot）时代已经来临。未来，人工智能有望在数学领域发挥更大的作用，甚至能发现新的数学定理。这项研究为解决大语言模型所面临的种种问题，开启了一个全新的篇章，也为推动人工智能在数学领域的应用提供了新的可能。

几天前，著名数学家、菲尔兹奖得主陶哲轩发布了一则令人瞩目的消息，他成功解决了一个数学难题，这一成就背后竟然运用了 cutting-edge人工智能技术 GPT-4。据悉，陶哲轩在探索解决方案的过程中，GPT-4为其提供了关键性的指导，使得他能够迅速找到问题的核心所在，从而顺利地进行后续计算。为了让更多的研究者借鉴这一经验，陶哲轩特意公开了他与 GPT-4 的对话记录，以期为我国科研工作者带来新的启示和灵感。

在当今数学界，越来越多的学者将焦点放在人工智能对数学领域的影响上，他们在各类研讨会中积极辩论，并运用各种AI工具来解决数学难题。据《纽约时报》对部分数学家的独家专访报道，这些数学家正努力面对人工智能这一最新的变革力量。自数千年前数学家们开始接触逻辑与推理以来，他们是否已做好迎接人工智能这一新挑战的准备呢？

数学家和计算机科学家一起开会

自两千多年前，欧几里得的著作成为数学论证与推理的标杆。卡内基梅隆大学的逻辑学专家杰里米·阿维加德在接受采访时指出：“欧几里得以富有诗意的‘定义（definitions）’开篇。” “基于此，他构建了当时的数学体系，采用基本概念、定义以及先验定理，每一个后续步骤都‘明确遵循’之前的步骤，从而论证事物的正确性。”阿维加德表示，虽然有人认为欧几里得的一些步骤不够显著，但其系统依然具有有效性。

但到了20世纪，数学家不再愿意将数学建立在这种直观的几何基础上。相反，他们开发了正式的系统——精确的符号表示、机械规则。最终，这种形式化使得数学能够转化为计算机代码。1976年，四色定理（该定理指出四种颜色足以填充地图，因此没有两个相邻区域具有相同的颜色）成为第一个借助计算强力证明的主要定理。

现在，人工智能来了。2019年，曾供职于谷歌、现供职于湾区一家初创企业的计算机科学家克里斯蒂安·塞格迪（Christian Szegedy）预测，计算机系统将在10年内赶上或超过人类最优秀数学家解决问题的能力。去年他将目标年份修改为2026年。

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

今年2月，阿维加德参加了在加州大学洛杉矶分校纯数学与应用数学研究所举办的“机器辅助证明”研讨会。这次聚会吸引了数学家和计算机科学家这一不寻常的组合。该研讨会的主要组织者是陶哲轩，他曾在一篇博客中称，2026年AI将与搜索和符号数学工具相结合，成为数学研究中值得信赖的合著者。陶指出，直到最近几年，数学家们才开始担心人工智能的潜在威胁，无论是对数学美学还是对他们自己，圈子成员现在正在提出这些问题并探索“打破禁忌”。

帮助解决数学问题的小工具们

如今，在饮食、睡眠、锻炼方面，优化人们生活的小工具十分普遍，威斯康星大学麦迪逊分校数学家乔丹·埃伦伯格（Jordan Ellenberg）在研讨会休息期间接受采访说：“我们喜欢给自己增加一些东西，以便更容易把事情做好。”人工智能小工具可能对数学有同样的作用。

其中一种数学小工具被称为证明助手或交互式定理证明器。数学家一步步将证明转化为代码，然后软件程序检查推理是否正确。验证在一个库中积累，成为其他人可以查阅的动态参考。阿维加德说，这种“形式化”为当今的数学奠定了基础，“就像欧几里得试图编纂和整理数学、为他那个时代的数学奠定了基础一样。”

最近，开源证明辅助系统Lean备受关注。Lean由计算机科学家莱昂纳多·德·莫拉（Leonardo de Moura）开发，当时他在微软，现在是亚马逊的计算机科学家。Lean使用自动推理，由所谓的“老式人工智能（GOFAI）”提供支持，即受逻辑启发的符号人工智能。到目前为止，Lean社区已经验证了一个翻转球体的定理和一个有助于统一数学领域的关键定理等。

但证明助手也有缺点：它经常抱怨不理解数学家输入的定义、公理或推理步骤，因此它被戏称为“证明抱怨者”。所有这些抱怨都会让研究变得很麻烦，但福特汉姆大学（Fordham University）的数学家希瑟·麦克白（Heather Macbeth）表示，提供逐行反馈的功能也使该系统对教学很有用。

今年春天，麦克白设计了一门“双语”课程：她把黑板上提出的每一个问题都翻译成讲义中的Lean代码，学生们用Lean和普通语言提交作业答案。 “这给了它们信心。”麦克白说，因为它们收到了关于证明何时完成以及整个过程中的每一步是对还是错的即时反馈。

自从参加洛杉矶研讨会以来，约翰·霍普金斯大学的数学家艾米丽·里尔（Emily Riehl）使用实验性证明辅助程序来形式化她之前与合著者发表的证明。在验证结束时，她说：“我真的非常深入地理解了这个证明，比我以前理解的要深入得多。”

约翰·霍普金斯大学的数学家艾米丽·里尔一直在使用一个实验性证明助理程序。

卡内基梅隆大学计算机科学家、亚马逊学者马利恩·海勒（Marijn Heule）使用另一种自动推理工具，被他称为“暴力推理”，或者更专业地说是可满足性问题求解器。他说，只要用精心设计的代码来说明你想要找到哪个“奇异物体”，超级计算机网络就会在搜索空间中进行“翻搅”，并确定该实体是否存在。

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

前谷歌计算机科学家、现在在湾区创业的宇怀·“托尼”·吴（Yuhuai “Tony” Wu）概述了一个更宏伟的机器学习目标。在谷歌，吴探索了支持聊天机器人的大型语言模型如何帮助数学。该团队使用的模型经过互联网数据训练，然后利用数学和科学论文的在线存档等大型数据集进行微调。吴在研讨会上说，当以日常语言来要求解决数学问题时，这个名为Minerva的专门聊天机器人“非常擅长模仿人类”。该模型在高中数学考试中获得的成绩优于16岁学生的平均成绩。吴说，他设想最终会有一位“自动化数学家”，具有“自行解决数学定理的能力”。

计算机科学家宇怀·“托尼”·吴设想了一位“自动化数学家”——具有“自行解决数学定理能力”的通用研究助理。

数学是试金石

对于这些颠覆式的创新，数学家们做出了不同程度的关注。

哥伦比亚大学的迈克尔·哈里斯（Michael Harris）表达了疑虑，他对研究数学与国防工业之间潜在的目标和价值观冲突感到困扰。在最近的一份时事通讯中，他指出由美国国家科学院组织的一个研讨班——“AI协助数学推理”中，一名演讲者是博思艾伦咨询公司（Booz Allen Hamilton）的代表，该公司是情报机构和军方的承包商。哈里斯希望，能够有更多关于人工智能影响数学研究的讨论。

DeepMind的合作者、悉尼大学的乔迪·威廉姆森（Geordie Williamson）在美国国家科学院的那场聚会上发表了讲话，鼓励数学家和计算机科学家更多地参与此类对话。在洛杉矶的研讨会上，他以改编自乔治·奥威尔1945年文章《你和原子弹》的一句话开始了自己的演讲。威廉姆森说：“考虑到我们所有人在未来五年内都可能受到深刻影响，深度学习并没有引起像预期那么多的讨论。”他认为，数学是机器学习能做什么或不能做什么的试金石。推理是数学过程的精髓，也是机器学习中尚未解决的关键问题。

威廉姆森在接受采访时表示，在他与DeepMind合作的早期，该团队发现了一个简单的神经网络，可以预测他非常关心的数学量，而且它的预测“准确得可笑”。威廉姆森努力想要理解其中的原因，但是无法理解，DeepMind的其他人也都做不到，而这个原因将成为一个定理的基础。就像欧几里得一样，神经网络以某种方式直观地辨别出了数学真理，但其逻辑“原因”却远非那么明显。

在洛杉矶的研讨会上，一个突出的主题是如何将直觉和逻辑结合起来。但威廉姆森观察到，人们很少有动力去理解机器学习的黑箱。他说：“这是科技界的黑客文化，如果它在大部分时间都有效，那就太好了。”但这种情况让数学家们感到不满意。

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