福建
近日Google DeepMind发布了AlphaProof Nexus，这个AI系统不仅能生成形式化证明，还能通过Lean证明助理的编译器进行自动验证，真正实现了“闭环”数学推理。
该系统自主解决了9个Erdős开放问题（共尝试353个），证明了44个OEIS猜想，并广泛的在优化理论、代数几何、图论、量子光学等多个领域协助解决了开放问题。其中两个Erdős问题已经悬而未决长达56年。
AlphaProof并非单一的AI模型，而是一个多Agent协作框架：
1. 基础生成-验证循环
每个“证明器子Agent”使用Gemini 3.1 Pro大模型，通过多轮对话迭代精炼证明草稿。每一轮修改后，Lean编译器立即反馈错误信息，形成“生成→编译→修正”的紧密闭环。
2. AlphaProof工具集成
子Agent可以调用AlphaProof——一个基于强化学习、已达到国际数学奥林匹克级别的定理证明系统——来处理数学上“常规但繁琐”的子目标。这就像人类数学家把计算交给计算器，自己专注于核心思路。
3. 进化式种群搜索
受AlphaEvolve启发，系统维护一个证明草稿数据库。子Agent从库中采样已有草稿进行“突变”和“杂交”，然后由专门的评级Agent（使用较便宜的Gemini 3.0 Flash）基于草稿的清晰度、合理性和新颖性进行Elo评分。这创造了一个“适者生存”的证明演化环境。
4. 全局目标缓存
系统会哈希每个待证明的子目标。一旦某个子目标被AlphaProof成功证明，结果会被缓存，供所有后续尝试复用，避免重复计算。
更关键的是AlphaProof还直接将证明成本打下来，成功证明每个Erdős问题的推理成本约为数百美元。
当然现在AlphaProof还存在许多问题，比方领域有限，目前成功主要集中在组合学、数论、凸优化等Lean的数学库已相当成熟的领域；大部分问题仍无法解决，尝试了353个Erdős问题只解决了其中的9个；证明中也经常出现幻觉。
但是AlphaProof Nexus的成果也表明，AI驱动的形式化证明搜索已迈入真正的研究级问题解决阶段。
以后数学家研究数学，必须会操控AI才行，否则很可能被替代，特别是数学专业里大量从事中低难度工作的，替代或许无法避免。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
