--- layout: post.njk source: https://yage.ai/share/anthropic-riemann-zeta-search-20260813.html speaker: yage.ai title: |- Anthropic 用 31M output token 搜索黎曼猜想，真正的信号在搜索架构 date: '2026-08-13' summary: Anthropic 在研究黎曼猜想时，利用 Claude 模型通过 31M output token 的工程化搜索过程，展示了如何将失败信息转化为资产，并建立搜索漏斗和五级验收阶梯。核心思想是AI在复杂数学问题上不再依赖多采样，而是通过设置测试驱动的终止标准和失败报告来收缩搜索空间，将搜索和验证解耦，从而在开放问题上实现有方向感的探索。 area: tech-engineering category: ai-application tags: - ai-search - search-strategy - agentic-workflow - formalization - failure-asset people: [] companies_orgs: - Anthropic products_models: - Claude media_books: [] draft: true status: evergreen --- 2026 年 8 月 10 日，Anthropic 发布了一项数学进展。他们拿一个未发布的研究版 Claude，把 Riemann zeta function 非平凡零点位于临界线上的比例下界，从 41.6% 提高到了 67.2%。看到这个数字第一反应可能是，AI 是不是快把黎曼猜想攻破了？其实不然。这里讨论的是 Riemann zeta function 的非平凡零点，而黎曼猜想要求 100% 的零点全部落在临界线上。Anthropic 自己也在文章里写得明白，这套技术走不到黎曼猜想的证明。 真正吸住我眼球的，是公开材料里拆出来的工程细节。两次 Claude Code session 跑下来，一共消耗了 31M output token，第二轮协调约 60 个 subagents，跑了 2400 条 shell commands，写了数百个 Python scripts，还下载了 54 篇 arXiv 论文。第一轮提出来的 650 个想法甚至全部失败了。最后交付到人类手里的，是一篇约 35 页的论文和一套 Lean formalization。算下来，这 31M output token 里绝大部分都在做路线搜索，真正用来写论文的只占最后一点点。 这正是我觉得最该拆开讲的地方。大家讨论 AI 做数学，注意力多半停在结果上：数字涨了多少，证明对不对，离黎曼猜想还有多远。但这次发布里真正有意思的，是 31M output token 怎么花出去的：系统怎样在未知路线里搜索，怎样利用失败信息，怎样把搜索和验证分成两个阶段。这篇文章要讲的就是这个过程，以及它暴露出来的一个更深的瓶颈。 搜索漏斗：从 650 个失败想法到少数成功路线，再进入验证阶梯 ## 搜索不是多采样 先从搜索和采样的区别说起。拿到 31M output token 去做数学，最容易想到的做法是让模型生成几百个候选证明，再拿个打分器挑最像的。但这套逻辑在复杂数学问题上很快就会撞墙。如果不根据前一步的结果去收缩搜索空间，就算采样一万次，也只是在同一个概率池里反复试投。 Anthropic 这里的做法更像搞工程，给每条路线设了类似 test-driven early fail 的 kill criteria。每条路线跑完之后，subagent 交回来的是一份死亡报告：这条路死在哪个前提上，哪些局部推导现在依然成立，以及后续出现什么新证据才允许重新打开。系统拿到这样的反馈，就能把撞墙路线的算力预算撤掉，挪去还没排查的方向。数学家平时啃硬骨头其实也是这个节奏，不断试探条件是不是下得太重、某种变换会不会在边界崩溃，或者把目标降级一步能推到哪里。每解决一个困惑，可行空间就跟着收紧一层。 公开材料里记了一段有意思的 hostile review。在最终路线敲定前，系统派出了三个互相隔离的 subagent，专门去攻击草稿里的证明。其中一个审查者真的抓到了一个隐藏的数学错误：草稿里 test system 的 mass matrix 建立在一个错误前提上，相关推导因此留下了一个真实缺口。关键是这个 subagent 不光指出了哪条假设失效，还直接给出了修复方案，搜索方向这才拿到了可执行的更新。 不过这里依然有个隐患挺突出。这套方向感到底来自同一个未发布的 Claude 模型家族。多 agent 并行能帮着减少单条推理里的偶然粗心，但大家底层的知识结构是一致的，碰到认知盲区很容易一起绕过去。跨模型家族的独立审查这次并未完全实现，这种相关性风险依然留在整个系统的验证链里。 ## 搜索什么、失败信息怎样变成资产 说到底，收缩搜索空间的前提，是得先弄明白系统到底在搜什么。我们平时写代码，搜索往往是在给定框架里调参。但数学里的搜索，找的东西要丰富得多。系统不仅要去找已有工具怎么拼接，还要试中间命题怎么改写、哪个量能压出更强的下界、哪条额外假设阻碍了无条件化，甚至还要设计 kill potential 最高的数值实验去快速扫盲。这次 Claude 抓过来的工具包里，就包括 Weil explicit formula、Montgomery pair correlation 以及 Bombieri 在二次型上的研究。 这次最关键的突破，其实是换了个看待对象的视角。以前的旧路线要求相关的数学量逐项为正，推导很容易卡死。Claude 换了个思路，它不再硬性要求整体结构全为正，转而去算里面到底包含多少个正方向。只要可用的正指标数量够用，结论就能成立。这一变，原路线里那些死板的约束立刻就松开了，这比沿着老公式机械地往下多算两步管用得多。 这种大范围摸索展现出一项工程优势，就是低概率路线的试错成本大幅降低了。人类数学家受限于精力与社区共识，很少会花几个月去硬砸那些公认希望渺茫的方向。但对模型来说，扫这些尾部路线只是算力分配问题。OpenAI 的 GPT-5 之前在 Erdős 单位距离问题 上也展现过类似的动作，数论学家 Arul Shankar 就提到，模型非常愿意去尝试那些社区觉得概率极低的路径。 更有意思的是第一轮那 650 个全盘皆输的想法。要是换作普通脚本，失败了就直接清零重来。但第一轮另留下了 106 个带有局部内容的 survivors，组了一份台账。这份台账远不是半篇证明，它详细记录着每条路卡在什么地方、为什么失败、哪一小段局部结论还站得住，以及重新开放需要什么新条件。到了第二轮，系统先去翻这份台账，对这 106 条旧路线逐个做 barrier check，确认缺口没漏掉，才去开辟新方向。失败信息就这么变成了 do-not-repeat list。 而且这些台账还能跨路线做垫脚石。材料里记了一个具体细节：第一轮留下的某个局部判断，起初看完全没用，结果 12 小时后在一条全新的路线上重新翻出来，正好补上了关键一步。推进下界数值也是靠副本接力完成的，一个 subagent 先把版本推到能证明 1/2 的位置，另一个并行 run 接着推到 2/3，最后靠精细优化摸到了 0.6725。从头到尾就没有哪个副本是一口气跑完全程的。 当然，公开材料目前只还原了这一条成功的路径，并没有把完整的路线转移图放出来。我们能确信的是系统确实记录并用上了失败资产，也确实发生了垫脚石转移，至于背后有没有形成更复杂的跨路线启发网络，现在还没有足够证据。 另外，聊这项成果的突破程度，绕不开窄盒条件。所谓窄盒条件，就是假设所有零点都贴在临界线附近的狭窄区域里。Baluyot、Goldston、Suriajaya、Turnage-Butterbaugh 这几位学者在 2024 到 2026 年的工作里，其实已经在窄盒假设下推到了 67.25%（arXiv:2501.14545；arXiv:2603.28104）。所以这 25.6 个百分点的跨越，不能全归为 Claude 从零发明的增量。它真正的实质贡献，是把窄盒条件给扔掉了，把已有的无条件 prime-side input 和 Weil 不定形式、Sylvester inertia 以及 rank-trace 读取拼到了起来。至于最终的历史优先权怎么算，还得等领域专家做最后的确认。 ## 验证链和五级验收阶梯 等搜索流程跑完、产出约 35 页论文和 Lean 代码之后，真正的考验才刚开始。要看懂这份交付物到了什么阶段，我们在分析 OpenAI 十项数学成果 时搭建过一套五级验收阶梯，拿来套这次的发布正好合适。这五级分别是：L1 候选已生成（有了论文或草稿）；L2 规则已检查（通过 Lean 编译、sorry-free 和公理审计等机器硬核检查）；L3 意图已对齐（形式化命题忠实表达了原始问题，没做悄悄降级）；L4 同行已理解（外部专家搞懂了核心逻辑和适用边界）；L5 共同体已吸收（成果进入主流文献，方法供后续研究复用）。 Anthropic 在 L2 上做得相当扎实。Lean 仓库 完整覆盖了 Theorems A-E 的核心渐近结论，证明代码里没有 sorry 占位；trusted challenge 中用于声明验收目标的 33 个 sorry 不进入 solution proof。顶层定理只依赖 Lean 的三项标准公理。他们还用 comparator 跑了 statement equality 检查和 kernel replay，甚至社区里也有人在固定 commit 上成功重放了构建。形式化命题直接挂在 Mathlib 的 riemannZeta 定义上，没有搞玩具函数凑数，机器检查确实对准了论文的核心对象。 但这里的代码覆盖也有两个明显的缺口。一个是论文里提到的有效形式 effective c(λ) 没有放进 headline statements，另一个是文中用于 31 项 SymPy 符号检查的 reference script 并没有丢进冻结仓库里。这些缺口倒不至于动摇主结论，但确实说明不能把形式化直接等同于论文里的每一句自然语言都被 Lean 跑透了。 到了 L3 这一级，目前算能守住，只是独立性稍弱了点。Anthropic 内部两位数学家 Alpöge 和 Furman 做了深度复核并承担了学术责任，还写了一份 informal note 方便同行快速抓重点。不过这两位都在 Anthropic 任职，意图对齐确实有人背书，但公开可审计的独立第三方人类复核目前还是缺席的。 至于 L4，现在只能算有一点早期信号。Brian Conrey 和 Dan Goldston 在短时间内看过了论文并给出了反馈，但截至发布后一天左右，并没有任何公开的审稿报告或者个人的公开技术评价。官方写的 “examined on short notice” 明确属于短时读稿，不能直接等同于正式的同行评议。至于 L5，发布才一天，共同体吸收自然还没发生。 把 Anthropic 这次的工作跟 OpenAI 那十项成果放在一起看，它的增量其实全在验收阶梯的前端。OpenAI 那会儿已有项目摸到了 L4 甚至 L5，比如非 sofic 群的证明机制很快有其他学者接过去构造新对象了。Anthropic 的贡献在于把 L1 之前的搜索漏斗给透明化了，让我们能清清楚楚地看到 650 个失败想法是怎么通过 kill criteria 和失败台账收敛出最终路线的，至于成果在验收阶梯上本身能走多远，并没有刷新纪录。 ## 瓶颈从搜索端移到吸收端 虽然单看 Anthropic 的成果并没有刷新阶梯后半段的纪录，但如果把最近这几个代表性案例放在一起比，会发现一个有意思的趋势：瓶颈正在从搜索端挪到吸收端。GPT-5 破局 Erdős 单位距离问题后，几位数学家花时间去整理、简化模型给出的原始逻辑，这才写出人类看得懂的 companion paper，随后 Will Sawin 又跟进把指数精炼到了 δ=0.014。模型先给出发现，人类随后花了更多工夫把它吃透。 OpenAI 那十项成果发布后，各个题目的消化进度也拉得极开，有的成果迅速跑到了 L5，有的却卡在 L2 动弹不得。陶哲轩主持的 IEANTN 项目 展现了同样的落差：AI 确实能把过去挂在社区好几周没人领的形式化任务缩短到几个小时跑完，但模型产出的证明过程太冗长、抽象层级也不自然，结果人类去审查和重构反而成了最费时间的部分。到了 Anthropic 这次，完整 campaign 跑了 54 小时、跨三个日历日，搜完路线并交出了 Lean 代码，而发布一天过后，数学共同体的吸收过程还没真正开始。 把这些现象放在一起看，趋势非常明确：生成和形式化的速度快速提升，但人类理解与吸收的速度几乎没变。只要生成端继续加速，整个研究系统的瓶颈就会顺理成章地从能不能找出来，转移到找出来之后大家能不能看懂、敢不敢认。 人类在研究链条里的角色也在发生变化。大家不再需要去干机械搬砖的活，精力转向了几个关键的对接点：挑选哪个问题有价值去攻击，盯紧形式化命题有没有偏离原始意图，把 AI 吐出来的笨拙证明改写成人类可读的范式，以及决定哪些产物有资格写入共享知识库。这些活全部踩在不同系统的交界处，单纯的代码或者文本生成在整个流程里的比重正在快速下降。 对我们搞 AI 系统设计的人来说，验证链上最核心的决策点其实叫作：什么东西可以晋升为共享前提。自然语言写的草稿，必须先收敛成对象、量词、常数都无懈可击的形式化声明，才能交给机器去比对证明项。要是少了形式化这层约束，约 60 个同家族的 subagent 极有可能只是在一堆模糊的散文里达成高度相关的幻觉共识；而一旦把这一层立起来，Lean 就能在 statement 和 definition 的边界上把大部分逻辑漏洞给卡下来。 不过形式化对齐最终依然需要人类来把关。Lean 的 kernel 既不知道代码有没有忠实表达论文的真实意图，也不知道外部学者早就利用窄盒条件做到了同样的常数。Claude 这次并没有证明黎曼猜想，67.2% 的新下界也只是这场发布展示出来的表象。更深层的信号是，AI 研究系统已经开始能在开放的复杂数学问题上做有方向感的搜索，并把极少数成功路线压缩成可审计的交付物。搜索和验证之间拉开的时间差，正在把越来越多的成本推到人类这一侧，接下来最昂贵、最难扩容的环节，就是理解与确认。