Google DeepMind 的 AlphaProof Nexus 把 353 个开放的 Erdős 问题啃下了 9 个——其中两道，数学界放了 56 年没动。这不是又一场"AI 在奥数题上刷分"的表演。区别有两处：题目本身是真正开放的研究级猜想；这批结果还走了同行评审，登上了《Science》。
Erdős 问题是个特殊物种。保罗·埃尔德什一生抛出上千个问题，题面常常一行写得完，证明却难到离谱。它们不要求你先建一套理论，只需要一个聪明的构造或一段严密的推理——这恰好是搜索型 AI 的主场。AlphaProof Nexus 走的是形式化验证的路子：把猜想翻译成 Lean 能读懂的语言，让模型在可自动检验的证明空间里反复试探，每一步当场判对错。错的分支立刻废掉，对的分支留下来继续长。这种"生成加验证"的闭环，比纯语言模型靠谱得多——数学不吃唬人的措辞。
但别急着宣布通用数学智能到来。9/353，命中率约 2.5%，剩下的 344 道可能只是更难，也可能是这套方法撞到了墙。Erdős 问题的口径很窄——短、自足、可形式化——它让这里成了 AI 最容易被检验的战场，而真正吃功夫的，是那些需要新框架、新定义的领域。数学界接下来该盯的不是这 9 个答案，而是这批工具会以多快的速度，被搬去啃剩下那 344 道。
