人工智能解决埃尔德什问题。接下来会发生什么？

仅仅几个月前，这个问题感觉主要是哲学性的: 如果人工智能可以帮助解决开放的数学问题，那么对人类天才的概念会发生什么变化?

那个问题不再是理论性的。最近两个涉及OpenAI和Google DeepMind的发展表明，人工智能正在从数学助手转变为数学参与者。不是在完全取代数学家的意义上，而是在生成、搜索、检查和有时发现能够经受住专家审查的论证的意义上。

第一个发展来自OpenAI，它宣布内部的一般推理模型在1946年由Paul Erdős提出的平面单位距离问题上取得了突破。这个问题询问在一个平面中可以有多少对点恰好相距一个单位。几十年来，人们普遍认为基于正方形网格的构造基本上是最优的。OpenAI的模型发现了一种新的构造家族，这种构造家族推翻了这种观点。

第二个发展来自Google DeepMind的研究人员，他们发表了一篇题为“使用AI驱动的形式证明搜索推进数学研究”的论文。他们的系统，AlphaProof Nexus，在开放的研究级问题上评估了AI驱动的证明生成，并报告说其最强代理自主解决了9个353个开放的Erdős问题。它还证明了492个来自在线整数序列百科全书的开放猜想中的44个。

这些结果一起标志着一个转变。重要的故事不是人工智能突然解决了数学。它没有。重要的故事是人工智能系统开始在研究循环本身中运作。

为什么Erdős问题是人工智能的严峻测试

Paul Erdős是历史上最多产的数学家之一，与他的工作相关的问题在数学中占有特殊地位。许多问题很容易表述，但很难解决，并且与组合数学、数论、图论和离散几何等深层次领域有关。

这使得它们对人工智能推理来说非常有用。它们不是学校练习。它们也不是总是像黎曼假设这样的巨大、理论破坏性的猜想。相反，许多Erdős问题处于中间地带，进展取决于找到正确的联系、正确的构造或正确的被忽略的引理。

这正是人工智能可能在早期最有用的地方。现代推理系统不仅仅是计算器。它们可以探索许多可能的证明路径，比较部分策略，检索来自邻近领域的遥远想法，并测试论证是否可以变得严谨。

OpenAI的结果很引人注目，因为该模型不仅仅是完善了一个已知的路线。它在离散几何和代数数论之间发现了一座意外的桥梁。这是数学家通常将其归因于真正创造力的概念跳跃的类型。

OpenAI和单位距离突破

平面单位距离问题很容易描述。将n个点放在平面上。计算有多少对点恰好相距一个单位。目标是了解随着n的增长，计数可以有多大。

近80年来，数学家们怀疑最佳构造不会明显优于基于正方形网格的排列。OpenAI的模型通过产生一个无限的例子家族来挑战这种假设，这个家族以多项式改进的方式优于预期的界限。

这很重要，理由有两点。首先，它改变了数学图景。它表明，数论构造可能比许多研究人员假设的更有可能为离散几何做出贡献。其次，它改变了人工智能的图景。所涉及的模型被描述为一个通用推理模型，而不是仅为这个特定问题而构建的系统。

换句话说，该系统似乎将推理能力转移到了一个陌生的研究环境中。它没有简单地记住一个已知的证明。它生成了一个外部数学家将其视为重大贡献的结果。

Google DeepMind和形式证明搜索

Google DeepMind的论文解决了一个不同但同样重要的问题：如何使人工智能生成的数学变得可靠？

语言模型可以产生看似优雅的论证，但其中可能包含微妙的错误。在正常的散文中，这些错误可能很难被发现。在数学中，一个错误的步骤可能会使整个证明无效。这就是为什么形式证明系统（如Lean）很重要。Lean不关心论证听起来是否有说服力。每一步逻辑都必须经过检查。

AlphaProof Nexus使用该约束作为工作流的一部分。人工智能代理在Lean中生成证明尝试，接收编译器的反馈，修改其方法，并继续搜索。更强的版本协调子代理，并使用更高级的证明工具来集中搜索。

DeepMind的结果尤为重要，因为它将人工智能推理与验证联系起来。该系统不需要像自然语言聊天机器人一样被信任。其证明要么编译，要么不编译。

这对数学研究意味着什么

当前的教训不是数学家已经过时。它是数学中的瓶颈可能正在改变。

历史上，研究人员需要做几乎所有事情：提出问题，调查文献，测试想法，构建证明，检查每一步，并传达结果。人工智能现在威胁着重新分配这种劳动。工作流程的一些部分可能会变得更快、更便宜、更自动化。

• 人工智能可以在人类投入时间到一个之前探索许多证明路线。
• 形式系统可以验证其他需要慢速专家检查的步骤。
• 研究人员可以使用人工智能在遥远的数学子领域中搜索。

这可能会产生一种新的研究风格。数学家可能不再要求人工智能提供答案，而是越来越多地监督证明代理。人类的角色变得不再像计算器，而更像研究主任：选择合适的问题，解释结果，检测概念的重要性，并决定哪些路径值得更深入地关注。

限制仍然存在

不应该夸大其词。Google DeepMind的系统解决了353个尝试的Erdős问题中的9个。这很令人印象深刻，但这也意味着大多数问题仍然未被解决。OpenAI的单位距离结果是一个里程碑，但这并不意味着每个著名的猜想现在都触手可及。

人工智能系统仍然难以处理需要新的概念框架的问题，或者相关的数学不够正式化，或者证明依赖于无法轻松分解为可搜索步骤的长链的洞察力。形式证明库也是不均匀的。具有成熟的Lean覆盖的领域比需要编码基础材料的领域更容易被人工智能代理访问。

• 这些系统仍然依赖于人类的问题选择和解释。
• 当定义模糊或不够发展时，形式化可能很困难。
• 人工智能生成的证明尝试仍然可能在未经证实的辅助声明中隐藏繁重的工作。

这些限制并不是失败。它们阐明了下一次进步必须发生的位置。更好的定理证明代理、更丰富的形式库、更强的验证工作流和更有效的人工智能接口都将很重要。

人工智能解决Erdős问题后会发生什么

最可能的近期未来并不是人工智能突然解决所有数学问题。它是人工智能辅助研究在具有清晰问题陈述、强大的形式库和大量分散的先前工作的领域中稳步扩张。

组合数学、图论、数论、优化和离散几何是自然的早期目标。这些领域通常包含问题，问题陈述简洁，但解决方案取决于从遥远的地方拼凑想法。人工智能非常适合这种搜索。

随着时间的推移，相同的模式可能会扩展到数学以外的领域。如果一个模型可以保持一个困难的论证，测试中间主张，并在领域之间连接想法，那些能力在物理学、生物学、材料科学、密码学和人工智能研究本身中都很重要。

更深层次的后果是文化的。数学一直重视证明，但也重视品味：知道哪个问题很重要，哪个抽象值得发明，哪个结果会改变一个领域的形状。随着证明搜索变得更加自动化，品味可能会变得更加重要，而不是不那么重要。

结论：天才向上移动

对早期问题的后续问题现在更加明确。如果人工智能可以解决开放的数学问题，人类的天才不会消失。它向上移动。

稀缺的技能将不再是单独完成每个技术步骤的能力。它将是提出正确问题、构建正确抽象、判断机器发现结果的意义以及引导人工智能系统朝着重要问题方向的能力。

OpenAI的单位距离突破和Google DeepMind的形式证明搜索结果并没有关闭人类数学创造力的书籍。它们开启了一个新的篇章，数学家可以在这个篇章中与能够比任何个人思维更快地探索领域的系统合作。

数学的未来可能不仅属于人类或机器。它可能属于那些学会如何让两者一起思考的研究人员。