当前，很多机器学习等AI工具正在帮助数学家创建新的理论并解决棘手的问题，这些AI工具正以超越单纯计算的方式改变数学领域。
图片来源：英国《自然》杂志网站
ChatGPT的横空出世让人们对聊天机器人的兴趣如野火般蔓延，数学家们开始探索人工智能(AI)如何帮助他们完成工作。英国《自然》杂志网站在2月17日的报道中指出，机器学习等AI工具已经帮助数学家创建新的理论并解决棘手的问题，它们正以超越单纯计算的方式改变数学领域。
“热度”空前
加拿大蒙特利尔大学的数字理论家安德鲁·格兰维尔表示：“我们正在研究一个非常具体的问题：机器会改变数学吗？”
不久前，在加州大学洛杉矶分校举行的一个研讨会探讨了这个问题，该研讨会旨在为数学家和计算机科学家之间架起桥梁。
2018年菲尔兹奖获得者、普林斯顿高等研究所的阿克谢·文卡特什早在去年10月的一次研讨会上，曾经进行过一场关于计算机将如何改变数学的对话。另外两位获奖者、巴黎法兰西学院的蒂莫西·高尔斯和加州大学洛杉矶分校的陶哲轩也对这一领域表现出兴趣。
英国帝国理工学院的数学家凯文·巴扎德表示：“菲尔兹奖获得者和其他非常著名的大数学家对这一领域感兴趣表明，这一领域的‘热度’与过去不同。”
各展所长
数学家们目前关注的一个方面是：哪种自动工具最有用。
一种是“符号主义”人工智能：程序员将逻辑或计算规则嵌入代码中，微软研究院的计算机科学家莱昂纳多·德·莫拉说：“这是人们所说的‘老式AI’。”
另一种是基于人工神经网络的AI，在过去10年取得了极大的成功。在这种类型的AI中，计算机或多或少都是从头开始，通过消化大量数据来学习，这被称为机器学习，它是包括ChatGPT等聊天机器人在内的“大型语言模型”的基础，也是可以在复杂游戏中击败人类玩家或预测蛋白质如何折叠的系统。
德·莫拉所在的微软研究院在2013年推出了计算机定理证明器Lean，帮助“符号”AI在数学领域取得了一些成就。
从原则上来说，Lean是一个“证明助手”，能帮助数学家完成证明过程：数学家可以把数学公式转换成代码，再输入到Lean中，让程序来验证定理是否正确。2020年，德国著名数学家、菲尔兹奖得主皮特·舒尔茨遇到的难题被Lean证明了。帮助舒尔茨只是Lean这么多年中的一项工作而已，这个数学证明器，如今已经得到许多数学家的支持。