数学界这个月彻底疯了！前脚OpenAI刚把Erdős80年的单位距离猜想推翻，数学家们的惊呼声还没落地，Google DeepMind就甩出了王炸——全新AI数学智能体AlphaProof Nexus，一出手就干掉9道悬而未决几十年的Erdős开放难题，最老的那道足足卡了56年！更狠的是，每道题的算力成本才几百美元，而且所有证明都被Lean编译器死死验证过，半点儿幻觉都没有！网友直接喊：数学奇点的火花，真的点燃了！
你可能还记得2024年那个拿了IMO银牌的初代AlphaProof，但这次的Nexus完全是“超级进化版”。把大语言模型（Gemini3.1Pro）、初代AlphaProof的强化学习树搜索，还有进化算法三者捏到一起，直接瞄准人类数学家啃不动的研究级难题。
它的架构分四层：AgentA是基础版，多个子智能体和Gemini对话修改Lean代码，编译器实时反馈错误，子智能体迭代修正；AgentB加了AlphaProof当工具，卡壳时调用树搜索攻克局部难点；AgentC引入进化算法，子智能体共享“草稿库”，LLM用Elo评分系统给草稿打分，高分的优先变异进化；AgentD是终极版，三者协同作战，就是它扫平了9道Erdős题。
整个流程像个永动机：AI提出证明草稿→Lean编译器验证→失败就反馈错误→AI修正→再验证，直到通过或算力用完。没有任何人类数学家介入，全靠AI自己搞定！
DeepMind用AgentD跑了353道形式化的Erdős题，每道最多3000轮迭代，结果9道被拿下。其中最重磅的是Erdős#12（1970年提出），56年悬案！多位数学家搞了半辈子都没完整构造，AI却用中国剩余定理和三项等差数列回避集，搭了一堆“精心设计的区块”就同时满足了密度条件和整除约束。
还有Erdős#125（1996年提出）：三进制下只用0和1的整数集A，加四进制下只用0和1的整数集B，它们的和集A+B下密度是不是正的？AI证明答案是否定的，下密度为零！核心是归纳稀疏化论证，利用log4/log3是无理数的性质，让密度以0.99的比率逐步衰减到零。
成本更惊喜：最便宜的152也才200-400美元。现在所有Lean证明代码都开源在GitHub上，随便看！
最让人跌破眼镜的不是AgentD有多强，而是最朴素的AgentA（只有LLM子智能体+编译器反馈）居然也能解决全部9道题！AgentB加了AlphaProof，表现和A差不多；AgentD只是在最难的题上（比如#125）成本低2-5倍。
DeepMind说，这归功于两个因素：一是LLM自身能力的飙升，二是编译器反馈能锚定LLM的推理方向。也就是说，随着基础模型越来越强，复杂的系统工程可能逐渐让位于简单的智能体循环。今天需要进化算法+AlphaProof才能高效解决的问题，明天可能一个朴素的LLM+编译器循环就够了！不过得用对模型，单独AlphaProof或小模型（比如Gemini3.0Flash）一道都解不出来。
AlphaProof Nexus可不是只盯着Erdős题。它还在多个数学分支搞出了大新闻：
2026年5月，AI在数学领域简直是“三路合围”：OpenAI用自然语言输出证明（但要人类专家验证），DeepMind用形式化验证（绝对可靠），还有AI辅助人类理解问题。即使智能体没证明出目标定理，它生成的形式化草稿也能帮专家聚焦未解决的子目标，不用重新验证整个论证链。
现在的图景很清晰：AI先用自然语言找思路，再用形式化系统固化验证，人类数学家从“亲手推导”变成“提问题、审方向、提炼洞见”。保罗·埃尔德什生前留了1217道难题，悬赏后人，他大概做梦都没想到，来领赏的会是AI吧？
你觉得AI会彻底改变数学研究吗？未来数学家会不会变成AI的“问题顾问”？评论区聊聊你的看法，转发给身边学数学的朋友，看看他们怎么说！
热门跟贴