OEIS Open：极简工具助大模型攻克147道数学猜想，解决率达44%
OEIS Open: How many conjectures can language models turn into theorems?
在数学研究的前沿领域，让人工智能自主发现并证明未决猜想，一直是检验大模型通用推理上限的核心标尺。此前，行业内偶有大模型攻克单一数学难题的战报，但由于尝试的问题空间未知、人类专家的介入程度未被公开，且缺乏标准化的统一基准，外界很难客观评估大模型在真实科研探索中的实际胜率与成本。
ArXiv URL：https://arxiv.org/abs/2608.11941v2
AI 评估机构 Epoch AI 近期发布了名为 OEIS Open 的开源基准，基于来自“在线整数序列百科全书”（OEIS）中由数学家提出且此前悬而未决的 492 个数学猜想。与以往依赖复杂进化搜索或特化定理证明系统的方案不同，这项研究采用仅配备终端命令、文本编辑器和资源监控工具的通用大模型，在 50 美元单题预算下自主解决了 147 道公开猜想，解决率达到 30%。在缩减版测试集 OEIS Open Lite 上将预算上限放宽至 200 美元时，前沿大模型的解决率进一步攀升至 44%。
这项研究不仅系统性地衡量了大模型解决开放数学问题的能力，更展示出两个关键事实：其一，形式化证明系统（Lean 4）彻底解决了此前开放数学基准中“验证器易错、单向、无法覆盖全称命题”的结构性缺陷；其二，复杂的智能体架构和庞大的外部文献库在定理证明上几乎没有带来收益，算力扩展法则（Inference-time Scaling）配合极简工具链，再次印证了计算领域的“苦涩教训”。
开放数学基准的困境与 Lean 形式化破局
构建面向“未决问题”的评测基准，核心难点在于结果如何自动验证。如果模型给出一个数学命题的证明，评测系统该如何判定其逻辑正确？
在此之前，业内主流的探索包括 HorizonMath 和 FrontierMath: Open Problems（FM:OP）。为了让未决问题能够被计算机自动化判卷，这两项工作不得不将题目严格限制在具有“生成器-验证器差距”（generator-verifier gap）的特殊问题类别中。这类问题的特征是：寻找解答非常困难，但验证一个候选答案的计算成本却很低。例如寻找满足特定极值条件的图结构、构造反例多项式，或者猜测某个数列的闭式解。
这种妥协带来了严重的评测局限：
绝大多数真实的数学研究命题并不存在这种验证差距。数学家提出的大量猜想要求对普遍适用的全称命题给出严密证明，而不是单纯寻找一个数值对象。如果无法把猜想压缩为一个能跑代码检验的输出，就无法纳入测试。
计算验证本质上只提供证据，而非严格证明。例如 HorizonMath 对闭式解的判定依赖高精度的数值比对，为了防止模型通过硬编码常数作弊，还必须额外引入大模型裁判进行二次审查；而 FM:OP 依赖研究人员为每道题手写的专用验证程序，不仅极其耗费人力，而且极易出现逻辑漏洞。在 2026 年 7 月，FM:OP 就曾因为验证器无法高精度识别正确解而被迫下架题目。
更根本的缺陷在于，单向的数值验证无法处理假命题。如果一个猜想本身不成立，且题目要求寻找满足猜想的对象，那么模型在该任务上注定无法得分。FM:OP 估计其题库中有 10% 到 40% 的问题实际上是无解的死胡同。
OEIS Open 改变了技术路线，要求所有解法必须提交为交互式定理证明器 Lean 4 中的形式化证明。每个猜想均已使用 Lean 形式化表述，大模型的任务是自主证明该猜想，或者证明其否定命题。
这种转向彻底化解了上述难题。评测的有效性不再依赖研究者为每个题目手写几十行易错的 Python 检验代码，而是直接交给 Lean 的底层逻辑内核进行类型检查与证明回放。为了防止模型通过环境漏洞或公理注入（Axiom Injection）作弊，评测框架引入了 SafeVerify 和 Comparator 两个独立的形式化校验工具，强制检查目标声明的名称、类型以及所使用的公理集合，确保模型提交的代码仅依赖 Lean 标准的三条经典公理（$propext$、$Quot.sound$、$Classical.choice$）。只要证明能编译通过，结论便具有严格的数学确定性；若猜想本身为假，模型证明其否定命题同样可以拿满分数。
极简框架的逆袭：通用大模型碾压特化系统
OEIS Open 中包含的 492 个猜想，源自 Tsoukalas 等人此前从 OEIS 中提取并借助模型辅助形式化的题库。在这项基准建立之前，唯一系统性尝试过该题库的系统是 Google DeepMind 团队构建的特化证明系统 AlphaProof Nexus。
AlphaProof Nexus 采用了高度复杂的工程设计：它基于 AlphaEvolve 演化算法，在共享的证明草稿群体上进行演化搜索。多个基于 Gemini 3.1 Pro 的生成子代理不断对草稿代码进行变异，针对编译报错的子目标，系统会调用专门在 Lean 证明树上执行树搜索的 AlphaProof 模块；未完成的证明草稿由于没有直接得分，系统又部署了多个 Gemini 3.0 Flash 评分代理从清晰度、新颖度等维度对草稿进行 Elo 天梯打分，利用类似 P-UCB 的算法决定哪份草稿优先获得计算资源。
然而，这一套耗费心血搭建的专用多代理进化搜索系统，在 492 道题目中最终仅成功证明了 44 道，成功率为 9%。
Epoch AI 采取了截然相反的设计哲学。他们搭建的基准代理（Base Agent）极其精简，仅仅是在开源评估库 Inspect 之上封装的一个标准 ReAct 工具循环，赋予大模型三个极其朴素的基础工具：执行命令的 bash 终端、读写文件的文本编辑器，以及一个查询当前剩余时间和 Token 预算的资源监控接口。沙盒容器内部预装了 Lean 4 环境（含 Mathlib 数学库）、SageMath 计算机代数系统，以及 SymPy、NumPy 等 Python 科学计算工具。
在这个完全依靠通用大模型自主决策的极简框架下，评测结果呈现了压倒性的优势：
在 492 道全量猜想上，单题设置 50 美元的花费上限，Claude Opus 4.8 独自攻克了 147 道猜想，成功率达到 30%；GPT-5.5 解决了 26%（128 道）；Gemini 3.5 Flash 解决了 22%（108 道）。在平均成本上，GPT-5.5 解决单个猜想的花费约为 6 美元，Gemini 3.5 Flash 为 9 美元，Claude Opus 4.8 为 10 美元。
在成功率提升两到三倍的同时，通用大模型单题的平均开销与 AlphaProof Nexus 维持在相近水平（后者平均解决单题成本约为 10 美元）。为了降低后续研究的评测开销，研究团队从题库中随机抽取了 100 道题目构成 OEIS Open Lite，并将单题预算上限提升至 200 美元。在 Lite 测试集上，最新一代的 Claude Fable 5 和 GPT-5.6 Sol 解决率分别达到了 44% 和 43%。
这种极简工具链对复杂特化系统的超越，展现了计算领域反复出现的“苦涩教训”：试图用人类先验的规则、精雕细琢的树搜索启发式以及繁复的子代理分工去约束问题求解，往往不如赋予通用基座模型简单直接的行动接口，让模型在庞大的推理算力支持下自主规划探索路径。
外挂文献与复杂代理为何统统失效？
在验证基准有效性的过程中，研究团队进行了两项具有重要参考价值的消融实验，分别探索了专业文献检索与复杂代理架构对高难度数学推理的助益。
第一项实验是为模型引入数学专业文献检索（Literature Variant）。研究团队打包了一个离线纯数学文献库，包含截至 2022 年上传到 arXiv 数学类别的 47.6 万篇论文的完整 LaTeX 源代码树。直觉上，科研猜想往往与已有学术成果存在千丝万缕的联系，如果模型能够自由检索相关论文，理应更快速地找到证明灵感或现成定理。
然而实验结果令人意外：接入 47.6 万篇数学论文后，所有受测大模型在 OEIS Open Lite 上的解决率没有任何统计学意义上的提升。
深入分析可以发现，OEIS 上的未决猜想虽然是开放的，但多属于高度特定的离散数学与整数性质问题。这类问题极少有前人撰写过可以直接搬用的定理段落，即便文献库中存在宏观相关的数论论文，模型通过搜索找到可用线索的信噪比也极低。在形式化定理证明中，真正的瓶颈在于从命题出发进行细致入微的符号推导、引理拆解以及将非形式化思路翻译为严格 Lean 代码的实现能力，文献检索带来的背景知识并未命中这一核心瓶颈。
第二项实验则是引入结构更繁复的智能体架构 DeepAgent。该变体不再使用单线程的 ReAct 循环，而是引入了子任务代理委派机制、跨轮次的持久记忆系统、结构化待办清单（Todo-list）工具，以及一段长而严苛的系统提示词（System Prompt）。
实验表明，DeepAgent 相比最简陋的单循环 Base Agent 同样没有取得任何优势。更复杂的控制流不仅未能理顺模型的证明逻辑，反而在多次上下文切换与代理间信息同步中引入了多余的开销。对于高度严肃且要求闭环验证的形式化证明任务，模型最需要的不是复杂的元认知组织形式，而是快速在终端中修改 Lean 代码、阅读编译器反馈并立即修正错误的紧凑迭代回路。
算力扩展法则：定理发现的对数线性增长
当消除了一切多余的脚手架之后，推动大模型定理证明能力提升的核心驱动力是什么？
实验给出了非常明确的信号：推理时间算力扩展（Inference-time Compute Scaling）。
研究团队追踪了模型在攻破猜想瞬间所累积消耗的费用，绘制出解决率与单题推演成本之间的关系曲线。数据表明，在对数坐标下，模型的猜想解决率随推演成本呈现极为稳固的线性增长趋势。粗略估算，在当前模型能力下，单题预算每增加十倍，猜想的解决率就会稳定提升约 10 个百分点。
更重要的是，在单题 200 美元的评测区间内，这条对数线性增长曲线完全没有出现平缓或饱和的平台期迹象。这意味着，当前 44% 的解决率远非模型能力的天花板。如果进一步放宽推演预算至数千美元，依靠大模型在沙盒环境中进行大规模代码变异、反例筛查与证明尝试，有理由预期更多沉睡在数学数据库中的猜想会被自动化攻克。
与此同时，研究也揭示了模型代际演进的现实状态。尽管 Claude Fable 5 和 GPT-5.6 Sol 拿下了 43% 到 44% 的最高分，但它们相比前一代旗舰模型（如 Claude Opus 4.8 的 40% 水平）的提升幅度仅有几个百分点。换言之，在面对全新的开放性形式化数学问题时，最新一代前沿模型并未表现出断层式的认知质变，目前的性能跃迁仍然主要受推演期长程搜索与算力预算的持续扩张所支配。
理性看待：未决猜想的含金量与评测局限
在审视大模型攻克 147 道科研猜想的亮眼成果时，必须保持客观审慎的科学视角。这批被攻破的问题，究竟在数学学术脉络中占据多大分量？
OEIS 作为一个开源的整数序列百科，虽然有严格的同行志愿者审查机制来剔除定义不清、无意义或拼凑的序列，但入库的开放猜想水平差异极大。Tsoukalas 等人在构建原始集合时，刻意过滤掉了黎曼猜想、孪生素数猜想等声名显赫的世界级难题，选取的是“非平庸、有数学趣味、但并非著名难题”的候选集。
通过对元数据的深层挖掘，研究团队揭示了这批猜想的真实生态：
在这 492 个猜想中，有整整 37%（182 道）由南京大学数学系教授孙智伟一人提出。作为极为高产的数学猜想提出者，孙教授在组合数论领域贡献了大量基于数值规律发现的猜想。
从文献引用角度来看，有 47% 的猜想所对应的序列，在 OEIS 条目内没有任何外部学术论文链接或参考文献记录；在 OpenAlex 全球学术论文数据库中针对这些序列进行全文检索，同样显示它们极少在主流文献中被正式讨论。
这说明，大模型目前批量攻克的问题，绝大多数属于此前“未被数学界充分分配注意力”的冷门分支。一个命题长期处于“未决”状态，往往不是因为它需要跨世纪的深邃理论突破，而是因为人类专业数学家尚未投入实质精力去处理它。大模型在这里扮演的角色，更接近于一个高效率的定理清洁工，在庞大的边缘猜想空间中快速清扫悬空结论。
此外，形式化评测本身也存在固有边界：
其一是自动形式化带来的翻译偏差风险（Misformalization）。这 492 道题目由大模型从自然语言数学描述自动翻译为 Lean 4 代码，尽管整数序列涉及的数学对象相对简单，比起高深代数几何不容易发生概念偏离，但仍难免存在翻译后的 Lean 命题比数学家原意更弱、或者因表述漏洞而变得极易证明的可能。此前 Tsoukalas 等人人工核对了系统解出的 44 题，未发现形式化错误，但这并不意味着剩余 400 余题全部完美保真。
其二是评价维度的单一性。在真实的数学研究中，将一个猜想规约（Reduction）为某个著名的世界难题（例如证明“猜想 A 蕴含考拉兹猜想”），往往会被学界视为盖棺定论式的重大突破。然而在 Lean 的自动化闭环评测中，这种极富学术价值的规约证明无法被判定为猜想成立或否定，系统只会给出失败结论。
最后是开放评测基准所必须面对的“数据污染半衰期”。一旦这 147 道猜想的 Lean 形式化证明被公开，未来的大模型预训练语料库势必会吸收这些代码。一旦解法泄露，基准题目的“未决”属性即刻失效，后续模型便无法证明自身是现场推导还是暗中复述。未来的基准维护者必须像流行病追踪一样，在评估新模型时动态剔除已被攻克并公开的题目子集。
自主科学发现的现实路径
Epoch AI 的这项工作为大模型时代的自动化科学探索确立了一个极具启发性的技术范本。
它证明了评估大模型前沿科研能力的最优解，不在于继续修补充满漏洞与人为偏见的传统判卷脚本，而在于全面拥抱以 Lean 为代表的形式化验证系统。形式化语言赋予了计算机绝对可靠的逻辑底线，使得大规模、低成本、防作弊的自动化科研竞赛成为可能。
更为关键的是，实验结果打破了“研究级推理必须依赖极其复杂的类人思维模拟架构”的工程迷信。面对严苛的证明搜索任务，一个极度精简的行动接口，配合充裕的推理期算力缩放，其产出效率远远胜过精心编织的专家系统。当通用大模型逐步掌握了操作形式化工具链的能力，将算力源源不断地转化为严谨数学定理的齿轮，已经开始实质性运转。