有价值的 AI 数学公告，应让读者还原结果：尝试了哪些问题？系统究竟证明了什么？谁确认形式化命题与原问题一致？AlphaProof Nexus 提供了较具体的审查材料，也说明为什么单看证明数量不够。
来源报道介绍了一项于 2026 年 10 月 8 日发表于 Science 的研究，其预印本在五月公布。论文报告：选定的 353 道 Erdős 问题中解决了九道，其中两道悬而未决 56 年；492 道 OEIS 猜想中证明了 44 道。这是针对预先准备题集的成绩，不能视为任意数学问题的成功率。
先看尝试范围
九除以 353，约为 2.5%。另外 344 道未完成的问题也应计入评价，因为它们揭示方法的现有边界。题目还必须先转写为 Lean，并得到现有形式化库支持。因此，题目选择、库覆盖程度和计算投入，与模型能力一起影响结果。
相关证据包括 Science 论文、预印本和公开证明仓库。成功文件支持逻辑核验，未成功的形式化题目则让评测范围透明，不会消失在标题背后。
区分三种正确性
Lean 检查证明是否符合已编码的定义和假设。这个保证很重要，但还需检查这些定义是否准确表达原问题。量词改变、边界条件遗漏，或增加更强假设，都可能使一个有效证明回答了更弱的问题。
新颖性需要另一次审查。旧定理可能已蕴含系统独立证明的结论。原报道提到，有审计质疑其中一个结果的新颖性。这不推翻其形式推导，却会改变可以宣称的新增研究贡献。专家回应解释了这一区别。
评估代理实际贡献
核心流程是生成 Lean 代码、进行检查，并根据编译反馈修改失败尝试。更复杂配置加入协同搜索及专用 AlphaProof 证明器。值得关注的是，报告中的最简单配置，在没有调用该专用工具的情况下，也解决了相同九道 Erdős 问题。
因此，在把成绩归因于复杂架构前，应查看消融实验。模型直接配合验证器的循环，可能解释大部分标题成绩。高级组件在其他任务中仍可能有帮助，但其价值应体现为新增成功、更低总成本或更好的研究支持。
为完整研究流程计费
成功的一次推理只是成本之一。失败搜索、命题形式化、库维护、专家审查，以及把形式证明解释清楚的工作，都属于成果的投入。遗漏这些项目的单次成功价格，不能代表完整发现成本。
研究团队试用时，应把问题陈述、尝试策略、可机器检查的产物、计算支出及人工干预一起保存。先审查形式化是否忠实，再核验逻辑证明，最后评估新颖性和解释价值，之后才宣称一个问题得到新解决。
更广泛的启示是代理设计方法：将概率生成与严格评估器结合，保存有用中间成果，把专家注意力用于自动检查无法覆盖的部分。原始报道支持这种边界清楚、也更实用的判断。进展应同时看独立审计、此前失败题目的改善和完成证明数量。