利用智能工具进行数学证明，还算是数学吗？加州大学洛杉矶分校纯数学与应用数学研究所举行了一次关于“机器辅助证明”（machine-assisted proofs）的研讨会，聚集众多数学家和计算机科学家。AI可能深刻改变数学的发展：算力会推动数学推理前进，但AI将对数学美感与数学家的身份带来潜在威胁。
在美国洛杉矶盖蒂博物馆（the Getty museum）的藏品中，有一幅17世纪古希腊数学家欧几里得（Euclid）的肖像：他蓬头垢面，用充满污垢的双手举着他的几何学著作《几何原本》（Elements）。
两千多年以来，欧几里得的理论成为数学论证和推理的典范。卡耐基梅隆大学（Carnegie Mellon University）的逻辑学家杰里米·阿维加德（Jeremy Avigad）认为：“欧几里得从‘定义’开始的著名论证，就像诗词一样优美。”
随后，欧几里得在此基础上建立了当时的数学体系，通过基本概念、定义和先验定理，让每一步论证之间都有清晰的逻辑关系。有人抱怨欧几里得的一些“明显”步骤并不明了，但这一套推理论证方式仍是奏效的。 但到了20世纪，数学家不再愿意将数学拘泥于这些直观的几何基础之上。
相反，他们发展出了通用的数学系统——精确的符号表达和机械的规则。逐渐地，这套形式化模式让数学得以被翻译为计算机代码。 1976年，四色定理（the four-color theorem，即可以仅用四种颜色来标注地图，相邻的两个地区都是不同颜色）成为第一个被计算机粗暴验证的重要理论。如今，数学家正努力应对一个最新的变革力量——人工智能。
克里斯蒂安·塞格迪（Christian Szegedy）是一名计算科学家，曾任职于谷歌，现就职于旧金山的一家初创公司。2019年，他预测在10年内，计算机系统的问题解决能力将相当或超过最优秀的人类数学家。去年，他将预测时间缩短至2026年。
阿克沙伊·文卡特什（Akshay Venkatesh）是普林斯顿高等研究院（Advanced Study in Princeton）的数学家，并在2018年获得了菲尔兹奖（the Fields Medal，数学界的诺贝尔奖）。阿克沙伊目前对AI并不感兴趣，但热衷于谈论相关话题。
在去年的一次采访中，他表示：“我希望我的学生能够意识到，自己所在的领域将会为世界带来很多改变。”他并不反对使用AI技术来帮助人类提高理解力，但关键在于要对技术的应用方式进行深思熟虑。
2月，阿维加德参加了在加州大学洛杉矶分校（the University of California, Los Angeles）纯数学与应用数学研究所举行的关于“机器辅助证明”（machine-assisted proofs）的研讨会。这次讨论会不同以往，聚集了许多数学家和计算机科学家。
该校数学系的任教老师陶哲轩（Terence Tao）在2006年获得了菲尔兹奖，也是这次会议的组织者。他认为这次会议具有重要意义。 陶哲轩指出，直到最近几年，数学家才开始担忧AI对于数学美学和自身的潜在威胁。会议中聚集的杰出学者正在讨论相关问题，并探索“打破禁忌”的可能策略。
会议中，有一位居于前排的参与者有些引人注目：这是一个名为“举手机器人”的梯形盒子，每当参会者提出问题时，它会发出机器低语并举起手。“如果机器人外表可爱且没有威胁性，那么就会有所帮助，”陶哲轩说道。
成为“证明抱怨者”的AI
现在有许多能改善我们饮食、睡眠、锻炼等生活方式的科技产品。威斯康星大学麦迪逊分校（the University of Wisconsin-Madison）数学家乔丹·艾伦伯格（Jordan Ellenberg）在研讨会茶歇时提出：“我们喜欢使用一些产品，让生活变得更加便利。” AI产品也可能为数学提供便利，他补充道：“很显然，问题在于机器能为我们做什么，而非机器将会对我们做什么。”
其中一个数学工具叫做证明助手或交互式定理证明器（数学辅助工具在1960年代早期就有所应用）。数学家逐步将证明转化为代码，然后通过软件程序检查证明是否正确。程序的数据库不断积累证明的相关数据并动态更新，以供其他使用者查阅。
霍斯金森形式数学中心（the Hoskinson Center for Formal Mathematics）主任阿维加德（Avigad）表示：“这样的形式为今天的数学奠定了基础，就像欧几里得当年所做的那样。” 最近，开源证明助手系统Lean引起了关注。Lean系统由微软计算机科学家莱昂纳多·德·莫拉（Leonardo de Moura）开发，他现在在亚马逊工作。
在GOFAI（Good Old-Fashioned Artificial Intelligence，即符号人工智能）的支持下，Lean能够进行自动推理。 到目前为止，Lean社区已经验证了有关将球体翻转的有趣定理、数学统一性中的关键定理等。 但证明助手也有缺点。它常常抱怨自己无法理解数学家输入的定义、公理或证明步骤，因此被称为“证明抱怨者”。
所有这些抱怨都会增加研究的困难。 但福特汉姆大学（Fordham University）的数学家希瑟·麦克白（Heather Macbeth）认为，该系统提供了逐行反馈，这也有助于教学。
在春季，麦克白设计了一个“双语言”课程，她将学生提出的问题在讲义中翻译为Lean代码，并让学生通过Lean寻找解决方案。
她表示：“这增加了学生的信心，因为他们能得到证明完成时间和正确性的及时反馈。” 自参加研讨会以来，约翰霍普金斯大学（Johns Hopkins University）的数学家艾米丽·里尔（Emily Riehl）使用实验证明助手验证之前与合著者发表的证明。
验证结束后，她表示自己对证明的理解更加深入了，思路也更加清晰，甚至能对一台傻瓜电脑解释自己的证明过程。
粗暴式推理，但这是数学吗？
卡内基梅隆大学计算机科学家、亚马逊学者玛丽恩·赫勒（Marijn Heule）使用了另一款自动推理工具，并将其称为“粗暴式推理”（或用技术语言来说是SAT求解器）。通过精心编写的编码来表达自己想要论证的问题，随后超级计算机网络就会进行推理论证。
在研讨会之前，赫勒和自己的博士生伯纳德·苏伯卡索（Bernardo Subercaseaux）针对一个长期性问题完成了一个大小为50TB的论证方案。然而，这个方案无法与赫勒及其合作者在2016年的产出相提并论——《自然》的一篇头条文章指出，这是一个有史以来最大的达到200TB的数学证明。
但文章接着提出，利用这些智能工具进行数学证明，真的算是数学吗？
在赫勒看来，智能辅助工具对于超出人类能力范围的问题来说仍是必需的。
其他一些工具采用了机器学习模型，能够梳理大量数据并检测相应的论证模式，但这些工具并不擅长逻辑的逐步推理。例如，谷歌的DeepMind设计了机器学习算法来解决蛋白质折叠（AlphaFold）和国际象棋（AlphaZero）等问题。
2021年，在《自然》的一篇论文中，研究团队将自己的产出描述为“在人工智能辅助下，提高人类的推理能力，进而推进数学发展”。 吴宇怀（Yuhuai Tony Wu）是一位计算机科学家，曾任职于谷歌，现在旧金山创立了一家初创公司。
他提出了一个更宏大的机器学习目标：解决数学问题。
在谷歌，吴宇怀探索了大型语言模型支持下的聊天机器人如何帮助解决数学问题。该团队收集互联网数据进行模型训练，并通过丰富的数学、科学论文等数据库进行调整，最终研发了专业聊天机器人Minerva。
被问及数学问题时，Minerva能够像人类一样进行解答。吴宇怀在研讨会上表示，该模型在高中数学考试中的表现优于平均年龄为16岁的人类学生。 最终，吴宇怀提出了自己的设想，设计一个有能力论证数学定理的“自动化数学家”。
数学是机器学习能力的试金石
对此，数学家表达了不同程度的关注。
哥伦比亚大学（Columbia University）的迈克尔·哈里斯（Michael Harris）对于缺乏有关人工智能对数学研究影响的讨论而感到遗憾，特别是与如今人工智能无处不在的热议话题相比。 悉尼大学的乔迪·威廉姆森（Geordie Williamson）是DeepMind的合作者，他鼓励数学家和计算机科学家更多地参与此类对话。
在研讨会上，他以改编自乔治·奥威尔（George Orwell）1945年发表的文章《你和原子弹》（You and the Atom Bomb）中的一句话来开始演讲：“鉴于在未来五年，我们可能会受到人工智能的深刻影响，深度学习还未引发足够的讨论。” 威廉姆森认为数学是机器学习能力的试金石。
推理是数学的精髓所在，而这也是机器学习尚未达到的能力。 在威廉姆森与DeepMind合作的早期，团队发现了一个能够准确预测数学问题的简单神经网络。威廉姆森尝试理解定理的论证过程，但团队都一无所获。就像古代几何学家欧几里得一样，神经网络以某种方式揭示了一个数学真理，却无法进行逻辑论证。
研讨会的一个主要议题是如何结合直觉和逻辑，如果人工智能能够同时做到这两件事，那么将对未来产生难以估量的影响。 但威廉姆森发现人们缺乏打开机器学习黑箱的动力，“这是科技界的黑客文化，如果这能推广到数学上当然很好”，但这不是数学家想看到的。
他补充道，探索神经网络的奥秘引发了“有趣的数学问题”，而这也为数学家提供了一个“为世界做出有价值贡献”的机会。
【竞赛报名/项目咨询请加微信：mollywei007】
