谷歌Deepmind推出的AlphaProof Nexus框架，结合大语言模型生成证明与机器核验技术，成功破解了诸多困扰数学界数十年的研究难题。

该全新框架自主挑战了 353 道悬而未决的厄多斯（Erdős）问题，顺利解开其中 9 道，包含两道长达 56 年无人解答的难题。

系统还完成了《整数序列在线百科全书》中 492 个开放猜想里的 44 项证明，解答了一道历时 15 年的代数几何希尔伯特函数相关问题，并优化了凸优化领域一项已知的数值边界。研究论文显示，该系统平均每道难题的推理成本仅数百美元。

与 OpenAI 近期采用的纯自然语言解法不同，AlphaProof Nexus 依托的基座模型为 Gemini 3.1 Pro。该模型无需独立梳理完整逻辑链条，而是先用Lean 形式化语言撰写证明步骤，再由编译器逐行核验；产生的报错信息会直接反馈给模型，用于新一轮推导。借助这种符号反馈机制，大语言模型的逻辑推理短板得到有效弥补，全程仅需人类在最终环节核验结果。

四类智能体，意外的实验结论

这套系统包含四款复杂度逐级提升的智能体：

• A 类智能体：架构最简单，基于 Gemini 3.1 Pro 运行多个独立子智能体并循环工作。模型生成证明步骤，Lean 编译器完成校验，报错信息持续回流迭代。
• B 类智能体：接入谷歌专为奥林匹克数学打造、基于强化学习的 AlphaProof 系统，补全证明过程中的缺失环节。
• C 类智能体：引入进化算法，灵感源自 AlphaEvolve。各子智能体共享证明思路库，由基于 Gemini 3.0 Flash 搭建的评分智能体，对思路的合理性与创新性打分，并采用埃洛评分体系完成排序。
• D 类智能体：整合以上全部功能，是功能最完备的版本。

研究团队最初使用 D 类智能体攻克厄多斯问题，但事后分析发现了意外结果：仅依靠大语言模型与编译器反馈的 A 类智能体，同样完成了这 9 道难题的证明，只是在处理高难度题目时成本更高。

研究人员认为，A 类智能体能够成功，主要得益于两大因素：基座大语言模型能力的飞速进步，以及编译器反馈对模型逻辑推理的正向引导作用。目前，全能型 D 类智能体在超难任务中仍具备优势，但随着大模型持续迭代，二者的差距或将不断缩小。研究团队表示，这也折射出行业趋势：随着大语言模型性能提升，专业定制系统正逐步向简易智能循环架构转变。

证明未果，仍具价值

该系统在组合数学、凸优化、数论等领域表现突出。这些领域的 Lean 数学库（Mathlib）发展成熟，复杂问题可拆解为多个易解决的子目标。不过研究人员坦言，绝大多数厄多斯问题依旧难以攻克，更不用说那些需要全新理论支撑的难题；同时，智能体也继承了大语言模型本身稳定性不足的问题。

即便未能完成完整证明，这套系统依然具备实用价值。参与测试的数学家表示，即便是失败的推导尝试，也能帮助人们加深对题目的理解。正如论文所述：“人工智能驱动的形式化证明检索，不仅能解题，更能助力人类深化认知。”

由于所有推导思路均采用形式化语言编写，科研人员无需从头复盘完整论证过程，可直接聚焦未解决的子问题。此外，该系统还能有效筛除文献中存在漏洞的形式化推导。论文指出：“形式化核验可作为筛选工具，判断哪些证明值得人工复核。”

目前，该系统已应用于量子光学、图论等前沿研究领域。项目所有 Lean 格式证明文件及部分自然语言证明内容，均已开源至 GitHub 平台。

厄多斯（Erdős）问题：AI 数学能力的试金石

如今，厄多斯问题已然成为衡量人工智能数学水平的标杆。此前，OpenAI 凭借自研推理模型，推翻了厄多斯单位距离猜想。菲尔兹奖得主蒂姆・高尔斯评价其为 “人工智能数学领域的里程碑”。在此之前，GPT-5.2 Pro 协助解开第 281 号厄多斯问题，数学家陶哲轩称这是 “大语言模型攻克公开数学难题最具说服力的案例”，后续 GPT-5.4 又成功解答了另一道厄多斯问题。

从某种角度来看，OpenAI 的成果难度更高。其模型全程依靠自然语言构建完整逻辑链，没有 Lean 编译器分步校验。而 AlphaProof Nexus 架构更规范、扩展性更强，定位是服务日常数学研究的实用 AI 工具。当然，OpenAI 也可将 Lean 技术融入自身框架，但他们的核心方向是测试大语言模型的原生推理能力。

陶哲轩也曾提醒大众，不必过度追捧相关热点。目前人工智能解答厄多斯问题的整体成功率仅 1%~2%，且集中在难度偏低的题目上。谷歌本次挑战 353 道题目仅解开 9 道，这一结果也恰好与 2% 的成功率相吻合。