陶哲轩弟子打造数学AI解决30年数学问题，为何数学家们说不算数？

近日，券商巨头 Robinhood 首席执行官弗拉德·特涅夫（Vlad Tenev）在社交媒体上发布了一条推文：“我们正处于数学领域深刻变革的风口浪尖。氛围证明（Vibe proving）的时代已经到来。”

他宣布，自己创办的人工智能公司 Harmonic 开发的 Aristotle 模型完全自主地解决了埃尔德什问题（Erdős Problem）124 号，这个数论猜想自 1995 年在学术期刊《Acta Arithmetica》上首次提出以来，已经悬而未决近三十年。

不到 24 小时后，埃尔德什问题网站的维护者托马斯·布鲁姆（Thomas Bloom）也发表了一系列评论。“这是一个很好的证明，完全由人工智能从形式化陈述出发、无人工干预生成，然后在 Lean 中形式化，这本身已经令人印象深刻，”布鲁姆写道，“事后来看，解决方案相当简单，使得这个问题处于数学竞赛题的水平。埃尔德什提出这个问题时有两个不同的版本。人工智能解决的是更简单的那个。”

埃尔德什问题 124 号问的是：给定一组整数 d₁, d₂, ..., dₖ，如果它们满足∑1/(dᵢ-1)≥1，那么是否所有足够大的整数都可以表示为一种特殊形式的和——每一项都是某个 dᵢ 的幂次，且该幂次在 dᵢ进制下只包含数字 0 和 1？在 1995 年的原始论文中，伯尔（Burr）、埃尔德什、格雷厄姆（Graham）和李文卿（Wen-Ching Li）明确排除了 1 的幂次，并附加了一个必要的最大公约数条件。但埃尔德什本人在后来的论文中重新表述这个问题时，却允许包含 1，并省略了最大公约数条件。Aristotle 解决的是后者。

“如果这样的简单方法有效，那么伯尔、埃尔德什、格雷厄姆和李这样的联合智慧肯定早就发现了，”布鲁姆写道。通常情况下，这会让他怀疑证明中存在被忽视的微妙之处，但由于证明已经在 Lean 证明助手中形式化，也就是说每一步推理都经过了机器验证，“显然它确实有效！”

证明该问题的普林斯顿大学数学博士鲍里斯·阿列克谢耶夫（Boris Alexeev）在讨论区详细描述了 Aristotle 的工作过程。他使用的是一个测试版本，具有增强的推理能力和自然语言界面。Aristotle 花费了 6 小时生成证明，而 Lean 的类型检查只用了 1 分钟。

值得一提的是，Aristotle 完全是从形式化陈述出发工作的，期间没有任何人工干预。只是阿列克谢耶夫发现并修正了形式化猜想项目中的一个打字错误——注释写的是“≥1”，而 Lean 代码却是“=1”。最终，Aristotle 证明了三个不同版本的问题。

Aristotle 的证明的确展现出一种令人意外的简洁美。一位名为 tsaf 的用户在讨论区用几行文字概述了核心思路：将所有 dᵢ 的幂次按升序排列形成序列 (aₙ)。例如，如果 d₁=2 且 d₂=3，序列就是 1, 1, 2, 3, 4, 8, 9, 16, 27, ...。

证明的关键是表明 aₙ₊₁-1 ≤ a₁+...+aₙ。如果这个不等式成立，那么通过归纳法，可以用前 n 项的子序列和来填“满”从 1 到 a₁+...+aₙ 的所有整数，而这个范围恰好足以覆盖 aₙ₊₁。

而关键就在于对 a₁+...+aₙ 这个总和的处理。将它改写为 ∑(dᵢ^(eᵢ,ₙ)-1)/(dᵢ-1)，其中 eᵢ,ₙ 是 dᵢ 在前 n 项中尚未出现的第一个指数。根据构造，aₙ₊₁ 恰好等于 mini(dᵢ^(eᵢ,ₙ))。由于问题假设 ∑1/(dᵢ-1)≥1，而 dᵢ^(eᵢ,ₙ)≥1，通过仔细计算就能验证所需的不等式。整个论证就是这几步推理，在 Lean 中的形式化证明也相对紧凑。

特涅夫的导师、菲尔兹奖得主陶哲轩也在讨论区出现了。他做了一个有趣的实验：将这个问题（简化版本）提供给谷歌的 Gemini Deepthink，并提示使用布朗准则（一个在加法组合学中常用的工具）。Gemini 宣称布朗准则不太可能强大到足以解决这个问题。

检查其推理过程后，陶哲轩发现这是一个“相当体面的错误”。Gemini 注意到，如果取 d₁=3，在 3^k 和 3^(k+1) 之间可能无限次地不存在任何其他 dᵢ的幂次，使得连续元素之间的比率可能高达 3。布朗准则通常需要连续元素的平均比率不超过 2，因此 Gemini 从启发式角度认为这种方法不太可能奏效。

“这实际上不是一个糟糕的分析，”陶哲轩评论道，“只是恰好所有小于 3^k 的其他幂次的累积和（勉强）足以克服 3 的间隙并最终到达 3^(k+1)。我会将这类错误归类为人类专家在这个问题上也可能犯的错误。”

他还指出，这种分析也暗示了为什么该问题的更强版本更加困难——在不允许 1 的情况下，序列的结构会发生根本变化，上述简洁的论证将不再适用。

陶哲轩进一步用庞梅朗斯（Pomerance）的观察来解释问题的微妙之处：通过丢番图逼近论可以证明，对于有限集合，条件 ∑1/(a-1)≥1 是必要的。但当这个和恰好等于 1 时，问题变得极其微妙，至少需要贝克定理（Baker's theorem）这样的深刻结果来防止不同底数的幂次聚集得太近，从而产生潜在的反例。

萨格勒布大学理学院数学系教授韦科·科瓦奇（Vjeko Kovac）也提供了另一个视角。他指出，在他与陶哲轩此前发表的一篇论文中的定理 2.3 可以被视为这个问题的连续参数变体，基本证明思路（排序序列、验证条件、考虑与每个参数相关的第一个出现项等）是相同的。

“我提到这一点并非要贬低 Aristotle 和阿列克谢耶夫的证明，恰恰相反，它非常漂亮，”科瓦奇写道，“我的观点是，基本思想在许多地方重复出现；人类常常未能意识到它们适用于不同的环境，而机器没有这个问题！我记得以前见过这个问题并简短地思考过它。我承认，我当时没有注意到这个联系，而现在对我来说却相当明显。”

科瓦奇的这段话也说明，Aristotle 找到的证明并非某种前所未有的创新技术，而是将已经存在于数学文献中的基本思想应用到了这个具体问题上。陶哲轩的实验进一步印证了这一点。

当他让 ChatGPT Pro 处理同样的问题时，该工具直接从埃尔德什问题网站上检索到了 Aristotle 的证明和 tsaf 的总结，并将其改写成人类可读的形式。陶哲轩注意到，可能存在关闭网络搜索的选项来测试工具独立解决问题的能力，但他没有探索这一点。

布鲁姆也提出了类似的疑问。他表示不会感到惊讶如果这个已解决的问题实际上曾出现在某个数学竞赛中，这样它可能已经是训练数据的一部分。在数学竞赛中，参赛者通常被告知一个简短优雅的解法是存在的——这正是 Aristotle 面对的情况。

问题在于，当四位数学家在 1995 年提出这个猜想时，他们并不知道是否存在这样的简单解法，而这种不确定性才是数学研究的常态。至于这个问题为何 30 年都没被解决，大概只是因为没有人真的认真尝试去解决它。

因此，就目前来看，Aristotle 确实能够在形式化的框架内探索证明空间，找到满足逻辑要求的推理链条。但这种能力更接近于在已知的数学工具箱中寻找合适的组合，而非发明全新的证明技术或提出原创的数学洞察。当基本思想已经在文献的某个角落存在时，人工智能展现出了发现和应用它们的能力；但当需要真正的概念突破时，情况可能会大不相同。

布鲁姆最终决定保持埃尔德什问题 124 号的“开放”状态，在主要陈述中保留最大公约数条件，并在备注中说明简化版本已被解决。阿列克谢耶夫对此表示同意：“Aristotle 解决了这个问题的‘一个’版本，但不是‘那个’版本。”这个微妙的区分，或许正是理解人工智能当前数学能力的关键。

参考资料：

1.https://x.com/vladtenev/status/1994922827208663383

2.https://x.com/thomasfbloom/status/1995094668879462466

3.https://www.erdosproblems.com/forum/thread/124

运营/排版：何晨龙