发生了什么
Google DeepMind 发表 AlphaProof Nexus(9 个 Erdős 问题)
为什么值得关注
建议重点阅读原文与论文细节，因为它不仅给出 9 个数学问题、44 个 OEIS 猜想等结果，还展示了“LLM + Lean 编译器反馈”这一更简单的 agent loop 在形式化证明中的有效性。
信息来源
以下内容来自公开来源，可打开原文继续核验。
01
AlphaProof Nexus 解 9 个 Erdős 问题
Google DeepMind 的 AlphaProof Nexus 通过将 LLM 推理与 Lean 形式化验证结合，自动解决了 9 个开放的 Erdős 问题，其中部分问题已悬而未决 56 年；单个问题的成本为“几百美元”。它还证明了 44 个开放的 OEIS 猜想，解决了一个 15 年前的代数几何问题，并在优化理论中发现了一个人类此前未找到的新算法参数。原文指出，一个更简单的 agent 仅通过交替进行 LLM 生成与编译器反馈，就复现了这 9 个 Erdős 成果；加入进化搜索和强化学习的完整系统，主要只在最难问题上带来明显优势。
打开原始来源 ↗