2025年3月，数学家丹尼尔·利特打了个赌。尽管人工智能在许多领域取得了长足的进步，但他相信自己的学科是安全的，并与一位同事打赌，到 2030 年，人工智能写出与人类最优秀数学家水平相同的数学论文的可能性只有 25%。仅仅一年后，他认为自己错了。“我现在预计会输掉这个赌注，”他在自己的网站上宣称。博客。

数学家们对人工智能解决问题和提供证明的能力的提高速度感到惊讶。“几年前，它们对于解决高中数学问题基本上毫无用处，而现在它们有时可以解决数学家研究生活中真正出现的问题，”多伦多大学的利特说。

这一进展比许多人预期的要快，数学家警告说他们的职业正在经历变革该领域有史以来最快的演变之一。“我们已经没有地方可以躲藏了，”写道杰里米·阿维加德最近在宾夕法尼亚州的卡内基梅隆大学论文。“我们必须面对这样一个事实：人工智能很快就能比我们更好地证明定理。”

引起这样反应的不是单一事件，而是人工智能正在展示的稳定的数学进展。去年，OpenAI 和 Google DeepMind 等公司实现了金牌表演国际数学奥林匹克竞赛是一项面向高中生的精英竞赛，许多专家此前认为该竞赛超出了人工智能工具的范围。一月份，数学家开始使用类似的工具解决匈牙利数学家 Paul ErdÅs 提出的长期问题。

现在，在两个独立的发展中，人工智能已经开始处理更复杂的数学问题，解决实际的研究问题并帮助自动验证尖端证明，而传统上这可能需要数学家团队进行大量工作。

二月，尼基尔·斯里瓦斯塔瓦加州大学伯克利分校的教授和他的同事启动了“第一个证明”项目，试图找到一个更现实的基准来测试人工智能的数学能力。第一轮项目包括研究人员在工作中需要解决的 10 个问题，这些问题来自截然不同的数学领域。

“它们是我们日常研究中自然出现的问题，”斯里瓦斯塔瓦说。– 它们是从典型的难度分布中得出的。它们并不是非常难，但也不是例行公事。确实有一个范围。”

进展证明

问题被公之于众后，解决方案开始涌入。OpenAI 和 Google DeepMind 等科技公司的研究人员试图用自己的 AI 模型解决“第一个证明”问题。OpenAI 声称，根据“专家的反馈”，它正确回答了一半的问题，而根据它针对每个问题咨询的数学家的说法，Google DeepMind 的得分为 6 分（满分 10 分）。

“事情变化得太快了，”说唐良在谷歌 DeepMind。“对于我们来说，现在人工智能已经真正成为一个严肃的合作者，要么可以进行严肃的研究工作，要么，就第一个证明而言，它实际上也可以自己提出解决方案。”

谷歌的 AI 数学工具名为 Aletheia，使用 Gemini AI 聊天机器人的计算密集型版本，并搭配验证算法来查找可能解决方案中的缺陷。然后它可以自行迭代地进行改进，直到得出答案。谷歌尚未公开披露 Aletheia 需要多少次迭代才能解决这些问题，这使得很难评估它到底有多好，但数学家们仍然印象深刻。

并非所有问题都被一致认为已得到解决。例如，对于属于几何学小众领域的问题 8，Google 询问的七位专家中只有五位同意所提出的解决方案是正确的。伊万·史密斯剑桥大学的一位未参与谷歌工作的人表示，人工智能似乎确实采取了明智的方法来解决这个问题，并显示出良好的进展。“如果这是一名博士生带着他们的想法回来，这将是令人鼓舞的，并且会让人相信结果是真实的，”史密斯说。

这凸显了人工智能生成的证据的一个问题——检查它们是一项艰苦的工作。很容易陷入这样一种情况：人工智能生成证据的速度比人类检查证据的速度还要快。如果一个定理被人工智能证明了，但周围没有人来检查它，它已经被证明了吗？人工智能在这方面也能提供帮助。

这项技术正在迅速改进，可以将自然语言的手写证明（例如《First Proof》中提出的问题）翻译成可以由计算机检查的格式，这一过程称为形式化。

人工智能公司 Math, Inc. 最近宣布，其名为 Gauss 的人工智能工具已经形式化了一项屡获殊荣的证明，并验证了其正确性，令数学家们大吃一惊。该证明涉及一个空间中可以容纳多少个球体，也是玛丽娜·维亚佐夫斯卡 (Maryna Viazovska) 2022 年菲尔兹奖（通常被称为数学诺贝尔奖）的主题。

2024 年底，一小群数学家开始了将 Viazovska 的工作正式化的工作，他们与数学部门分开工作。Inc，他们希望手动将问题转化为计算机代码。他们首先研究了 Viazovska 的八维球体堆积解决方案。当他们取得稳步进展时，后来为研究人员提供帮助的 Math, Inc. 宣布它已经有了完整的证明，然后是 24 维结果的更通用版本。

巴维克·梅塔伦敦帝国理工学院的伦敦大学教授和他的同事最初草拟了如何将这项工作形式化的粗略计划，并提出了重要的数学定义。梅塔说，如果没有这个，人工智能就无法完成其证明。

“我们已经制作了所有部件，但我们还没有编写说明如何将它们组合在一起的说明手册，”说克里斯·伯克贝克英国东安格利亚大学的教授也是该团队的成员。

新数学家风格

最终的证明大约有 200,000 行代码，约占所有现有形式化数学的 10%。尽管这段代码可能比人类完成相同任务所需的代码长大约 10 倍，但这仍然是一项巨大的成就，他说约翰·科梅林在荷兰乌得勒支大学。——这是一件大事。这是获得菲尔兹奖的作品，并且正在自动形式化。”

科梅林表示，类似的努力现在应该可以在许多其他领域进行，这可能会改变数学的实践方式。“我们都在考虑的未来是，我们将拥有能够自动形式化新研究和数学论文的工具，并标记是否存在错误，”Commelin 说。“这将对同行评审和评审工作产生巨大影响。”

面对人工智能完成越来越多的数学工作的未来，像阿维加德这样的一些数学家正在发出警报，担心这可能会对我们练习和提出新数学的能力产生不利影响。

说，使用机器解决第一个证明中提出的问题类型可能会产生具体的证明安娜·玛丽·博曼她说，我们在田纳西州范德比尔特大学学习，但我们失去了“学习机会”。– 努力创造和阐述新思想并解决新问题是学生和数学专业人士巩固知识的主要方式之一。 –

冯托尼谷歌 DeepMind 的 Aletheia 团队成员之一也有类似的感受，并且自己对使用该工具持谨慎态度。– 很多时候我觉得我应该做自己的作业并经历建立自己直觉的过程。 –

Mehta 表示，即使是形式化的证明也可以产生重要的见解，他和他的同事现在需要理清 200,000 行 AI 证明，以找出可能对其他项目有用的内容。

但数学家们仍然希望它们能够在日益机器主导的未来中占有一席之地。回顾历史，科梅林说，手动计算曾经是数学家的重要组成部分，但现在它们是自动完成的。“我认为类似的事情也会在这里发生，我们从根本上改变我们正在做的事情，但从现在起 10 或 20 年后，我们仍然会以一种新的方式将我们正在做的事情视为数学。”