编辑推荐：
人工智能在数学领域的应用取得显著进展，从ChatGPT的早期算术缺陷到大型语言模型如o4-mini在竞赛中的优异表现。数学家开始利用AI进行探索性研究，如DeepMind与Williamson的协作项目，通过神经网络揭示复杂数学结构中的隐藏规律。同时，符号AI工具如Lean被用于形式化证明，推动数学知识的大规模数字化（如Mathlib和ETP项目）。尽管AI展现出辅助研究潜力，但数学家仍对AI取代核心创造性工作存在担忧，并强调需通过严格基准测试和合作机制保障学科发展。
2022年秋季，随着ChatGPT的问世，人工智能（AI）开始进入公众的视野。尽管ChatGPT在语法处理方面表现出色，但其数学能力却相当糟糕。当被要求进行简单的数学运算（比如加法）时，它可能会给出一串数字，其中开头和结尾的数字是正确的，而中间的数字则是随机生成的。这显然表明：AI目前还无法胜任数学计算任务。
快进到2025年，ChatGPT不仅在算术能力上有了显著提升，而且那些具备更强推理能力的大型语言模型（LLMs）也开始在学校的数学作业中表现出色，并在数学竞赛中获奖。
不过，AI在数学领域真正取得的进步体现在数学家们开始将其应用于研究之中。数学是一门历史悠久的学科，而AI则是新兴技术，但两者之间存在着深厚的契合度。AI公司意识到了这一点，并开始与数学家们合作——许多数学家此前与任何形式的技术都几乎毫无交集。
卡内基梅隆大学哲学与数学科学教授、霍斯金森形式数学中心主任杰里米·阿维加德（Jeremy Avigad）表示，数学家们对AI充满兴趣和好奇。同时他也提到：“人们对AI如何改变数学领域，甚至可能取代某些被视为数学核心的概念感到担忧。数学界仍在努力理解这项技术，并决定如何利用它。”
数学的研究方式
数学家们通过研究抽象对象和结构，寻找其中的显著特征（如形式、模式和对称性）来进行工作。他们会通过举例分析、绘制图表以及进行计算来探索各种可能性，这一过程在很大程度上依赖于直觉。
然而，一旦数学家们取得新的发现（即提出一个新的定理），接下来就需要撰写严密的证明。虽然证明是用自然语言撰写的，但其整个推理过程原则上都可以被严格验证，直至最基础的逻辑层面。
数学研究的探索性和严谨性在两种类型的AI中都有体现：一种是基于神经网络的AI（如机器学习），它通过处理大量数据来发现隐藏的模式和规律；另一种是基于符号系统的AI（如形式化证明助手），它通过逻辑推导得出精确的结论。
阿维加德指出：“AI在数学领域的魅力在于它结合了机器学习和符号方法的优势。如果能够将这两种技术融合在一起，就能实现两全其美的效果：系统既能具备处理复杂问题的经验和直觉，又能提供正确的证明和解释。”
神经网络AI带来的直觉
在探索阶段，数学家们通常使用黑板、笔和纸进行工作，有时也会借助计算机代数或图形软件辅助。不过近年来，一些数学家开始利用神经网络来增强他们的探索能力。
例如，澳大利亚悉尼大学的乔治·威廉姆森（Geordie Williamson）与DeepMind的研究人员合作，他们在表示论领域研究了特定类型的图与单变量多项式（Kazhdan-Lusztig多项式）之间的关系。前者是由节点和边组成的复杂结构，而后者虽然表达形式简单，但其中蕴含的信息却难以提取。
DeepMind利用大量数据训练神经网络，使其能够高精度地预测这些多项式。分析显示，某些图中的边在预测中起着关键作用，这一发现揭示了图中之前未被注意到的结构。威廉姆森随后用传统方法证明了图与多项式之间的联系。这是AI在数学领域的一个创新应用，也为后续研究提供了启发。
在2023年6月美国国家科学院举办的AI与数学研讨会上，威廉姆森提到了这项工作面临的一些挑战：比如技术实现的细节问题可能导致结果错误，他怀疑这可能是算法本身的问题还是实施不当所致。他也表示，AI为数学研究带来了新的视角。
符号系统AI带来的严谨性
在研究的后期阶段，数学家们更注重清晰性、严谨性和准确性，这时符号系统AI发挥了重要作用。
近年来，一种重要的符号AI应用是定理的形式化表达，即用逻辑系统的形式化语言和语法来表述定理。类似软件验证工具，证明助手可以验证这些形式化的证明。虽然将自然语言证明转换为机器可理解的形式化证明是一个漫长而繁琐的过程，但随着新工具的出现，证明助手在数学界逐渐得到认可。
最常用的证明助手之一是Lean，它由莱昂纳多·德·莫拉（Leonardo de Moura）在2010年代初开发，目前由亚马逊网络服务公司维护。Mathlib是一个基于Lean的电子知识库，包含约10万个定义和25万个定理，涵盖了标准本科数学课程的内容以及大量新旧研究成果。
Mathlib未来的应用方向尚不明确，但正如英国帝国理工学院的凯文·巴扎德（Kevin Buzzard）所言：“Mathlib正在‘数字化’数学——就像Spotify数字化音乐一样。虽然还不确定具体会带来什么变化，但我相信这肯定会改变数学领域。”
加州大学洛杉矶分校的菲尔兹奖得主陶哲轩（Terence Tao）领导的Equational Theories Project（ETP）项目则尝试通过大规模计算生成新的数学知识。该项目专注于代数结构方程之间的逻辑关系。对于最多包含四个变量的方程，存在大约4700种这样的关系。50名团队成员在不到六个月内利用强大计算资源找到了所有这些关系。
陶哲轩指出，传统上数学家通常是逐一解决问题，而ETP则通过团队协作快速生成了大量新知识。他称：“仅靠人类是无法完成这项工作的。”
安德烈·鲍尔（Andrej Bauer）开玩笑说，未来ChatGPT可能会生成大量虚假的数学论文，干扰真正的数学研究。不过他相信，机械化的验证机制（如Lean）有助于确保结果的准确性。
LLMs的进步
未来大型语言模型（LLMs）能否将神经网络AI和符号系统AI结合起来，服务于数学研究？虽然有可能，但那还需要很长时间。在2025年的国际数学奥林匹克竞赛中，LLMs取得了优异成绩，但比赛题目仍局限于高中数学水平。
随着LLMs在这些任务上的不断进步，现在需要更具有挑战性的测试标准。2025年，一个由40位数学家组成的团队在FrontierMath非营利组织的支持下制定了新的测试标准。
这些测试题难度较高，需要数学家掌握相关文献并运用多种非传统方法。它们并非陷阱题，而是为了检验AI的能力和局限性。例如，测试结果需要是一个难以猜测的数字。
每个测试题的制定都是一项平衡工作。参与开发的肯·奥诺（Ken Ono）表示：“找到让模型真正动脑筋的问题非常困难。”2025年12月，奥诺离开了学术界，加入了一家AI初创公司Axiom Math。
在2025年5月于伯克利举行的FrontierMath会议上，奥诺看到自己设计的测试题被ChatGPT的升级版本o4-mini成功解决。他说：“AI能在短短10分钟内独立完成这个问题，确实令人印象深刻。”
新工具带来的新挑战
奥诺还提到，与o4-mini的互动让他感到既兴奋又担忧：他可以让AI总结已知的研究方法，并将其应用于完全陌生的数学领域。虽然AI在某些方面很有帮助，但真正的创新仍依赖于数学家自身的创造力。
尽管这些工具非常实用，奥诺指出：“目前还没有AI生成的完全原创的数学成果。”他认为，真正的数学创新来自于数学家自己提出的新概念和联系。
阿林·杰克逊（Allyn Jackson）是一位专注于科学和数学领域的德国记者。
