10月27日前后，AI圈出现了一件很罕见的事：OpenAI和Anthropic各自宣布，它们的模型给出了一个长期存在的复杂性理论猜想——指数时间假设（Exponential Time Hypothesis）的反证，核心结果据称都指向10月16日。OpenAI还同时宣布了调和分析、复杂性理论和量子场论方向的新结果，并表示证明已交给外部专家核查。两家竞争对手在同一问题上得出同一结论，这本身就值得注意；但更值得注意的是，数学界的反应出奇地克制。
先分清两件事：AI“想出证明”，和机器“验算证明”
这次讨论里最容易混淆的，是两个不同的环节。一个是“发现”：模型是否真的找到了正确的证明思路；另一个是“验证”：用Lean这样的形式化工具，把证明写成机器能逐行检查的形式。Lean能保证的是“写下来的定理，在写下来的定义之下，逻辑上没有跳步”，它不能保证“这个定理就是数学家原来想问的那个问题”。所以有报道指出，相关工作组的参与并不等同于认证，外部审查可能需要几个月。这不是泼冷水，而是数学的正常流程：一个几十年的猜想，不会因为一份机器检查通过的文件就当天盖棺定论。
为什么两家同时“证否”，反而更需要慢下来
两家独立得出同一结论，确实提高了可信度，但也提出了一个新问题：如果AI的证明思路高度相似，是不是因为它们在相似的数据和训练方式下走到了同一个地方？这并不意味着结论是错的，而是意味着“独立验证”的含金量需要重新评估。真正的验证，来自不依赖同一套模型的数学家：他们要检查定义有没有被悄悄改动、引理有没有循环论证、边界条件有没有被偷换。这些工作快不了，也急不得。
对普通人来说，这件事的真正启示是什么
不是“数学家要失业了”，而是“数学研究的工作流要变了”。AI正在变成一个很强的“猜想生成器”和“草稿撰写者”，它可以在短时间内提出人类需要很久才能想到的路径；但“这个证明到底对不对”，仍然需要人类数学家用几个月的时间去抠。未来的数学论文，可能会越来越多地出现“AI辅助发现、人类主导验证”的署名方式。AI把探索的速度提上去了，验证的严谨性反而变得更重要，而不是更不重要。
写在最后
AI证否一个几十年猜想，值得兴奋，但不值得立刻下结论。科学史上，真正站得住的突破，从来不是“宣布得最快”的那个，而是“经得起最慢审查”的那个。这一次，AI证明了自己的探索能力；接下来几个月，数学界的审查会证明这件事到底算什么。
