数学家的Deep Blue时刻？OpenAI用不到2000美元破解了十个十年未解难题

这几天AI在数学界连续投下两颗震撼弹。先是Anthropic用Claude模型挖掘密码学弱点，砸了10万美元，要求“别找软柿子，要真正的硬货”。紧接着，OpenAI就晒出了更惊人的成绩：用内部新一代模型Astra，以每个问题不到2000美元的成本，解决了十个至少十年无进展的数学难题。

这像极了当年深蓝击败卡斯帕罗夫的那一刻——但这次，被震撼的是数学家。OpenAI没有透露他们尝试了多少问题才得到这十个解，但公布的所有证明都已用Lean 4严格形式化，还附带了论文和一份由模型自己生成的“推理思路复盘”。这手透明度算得上体面，可人们最关心的提示词依旧藏在黑匣子里。

为什么这件事现在发生？

其实这不是AI第一次渗入数学。近几年，从符号回归到自动化定理证明，AI一直在边缘试探。但过去多是辅助：帮人检查错误、搜索已知定理。这次不同。Astra模型直接端到端地给出了原创证明，而且难题是精挑细选的——那些人类顶尖头脑卡了十年的硬骨头。这意味模型的推理能力已经跨过了某个阈值，开始真正“做研究”。

数学家Kirwin Hampshire在上一波较弱的AI数学成果出来后，就写了一篇《数学的暗夜》，描述一种“深刻的精神危机”。当看到OpenAI的新成果，这股情绪恐怕会加倍蔓延。但另一边，菲尔兹奖得主陶哲轩却给出了更开放的视角。他在IEEE Spectrum的访谈中提出“大数学”概念：未来数学将是大规模、去中心化的人机协作，人类负责创意部分，AI负责技术苦活。

到底改变了什么？

这次事件最核心的启示是：AI不再只是翻找现有知识的搜索引擎，它开始具备“发现”的能力。而且成本极低——2000美元对于一个数学问题的突破来说，几乎可以忽略不计。这意味着大规模、自动化地探索数学猜想可能很快成为现实。过去一个博士生花几年才能验证的方向，现在也许一顿午饭的时间就能看到初步结果。

但恐慌也并非多余。如果模型真的能独立产出有意义的数学证明，那么数学家作为“真理发现者”的独特身份会动摇。不过，仔细看OpenAI公开的推理复盘，会发现模型的思路虽然有效，但常常显得“反直觉”甚至“古怪”，就像阿尔法围棋走出人类从未想过的着法。这恰恰说明，AI不是在模仿人类思维，而是在发展另一种智能形式。

我们该怎么看、怎么用？

对于AI从业者，这提供了一个观察前沿模型能力的宝贵窗口，暗示着推理能力的下一次跃迁可能已经不远。对于数学研究者，更现实的态度或许是把这类工具纳入日常工作流：用它快速筛选题思路、生成反例、甚至在证明瓶颈处提供灵感。陶哲轩式的“大数学”协作，可能正是消解恐惧的最佳路径。

这件事也打破了一个常见错觉：很多人以为AI会先替换重复性的体力劳动，创造性工作最安全。但现实是，AI正在用极低成本冲击人类引以为傲的智力高地。不是因为它理解了数学，而是因为它掌握了某种我们还没定义好的“推理”。这或许才是真正的深蓝时刻——不是机器赢了人，而是机器逼我们重新定义什么是赢。

原文地址: Ten advances in mathematics and theoretical computer science