百年难题没解开，但一个卡了三十多年的数字被一步推高。Anthropic 公布了完整过程、审稿名单和一份 Lean 形式化证明。
消息来自 Anthropic 8 月 10 日放出的一份研究说明。需要先把预期按住：黎曼猜想没有被证明，短期内也不会因为这件事被证明。但对做解析数论的人来说，67.2% 这个数字本身足够刺眼。
黎曼猜想的表述很短：zeta 函数所有非平凡零点，实部都等于 1/2，也就是全都落在那条"临界线"上。100% 目前证不出来，于是从上世纪七十年代起，数学界走了一条退路——先证"至少有百分之多少落在线上"。
这条退路本身就是一部小史。Levinson 在 1974 年拿到三分之一，Conrey 在 1989 年推到五分之二（40%），此后三十多年里，几篇论文一点一点往上挪，公开记录长期停在 41.6% 附近。每提高零点几个百分点，都是一篇正经论文的分量。这次一步跨到 67.2%，等于把"过半"这道心理线直接越了过去。
过程被写得比结果还细。据 Anthropic 说明，Claude 是在 Claude Code 里以多代理方式跑的：约 60 个子代理协同、数千次数值检验、约 2400 条 shell 命令，累计 3100 万输出 token，耗时一天半。
但真正起作用的不是这些数字。按官方描述，关键的一步是换了个看问题的角度：以往把"线上的零点"和"线外的零点"分开处理，这次把两类零点放进同一个几何空间里统一考虑，推出的不等式更紧。整项工作也不是凭空起跳，它建立在 Baluyot、Goldston 等人近年研究的基础上。
Anthropic 内部两位数学家先复核了论文，数论学者 Brian Conrey 和 Dan Goldston 也在很短时间内读完并给出意见。这份名单值得多看一眼——Conrey 正是 1989 年那个 40% 纪录的作者，让他来审一份把自己的纪录几乎翻倍的稿子，比任何基准分数都更说明问题。
除论文外，Claude 还生成了对应的 Lean 形式化证明。这一条容易被当成技术细节略过，却可能是整件事里最实的部分：机器产出的数学，长期瓶颈从来不在写，而在验——一份几十页的新证明，找够格的人逐行读完要花掉数月。有了形式化版本，机器可以自己检查每一步是否成立，人的工作缩减到确认定理的陈述有没有写歪。
Anthropic 自己压低了这层联想：这条技术路线并不指望直接通向黎曼猜想的完整证明。从 67.2% 到 100% 不是再加把劲的问题，中间隔着方法论意义上的断层——现有这一族"占比下界"的工具被普遍认为存在天然上限，堆多少算力都跨不过去。
真正改变的是另一件事。过去衡量模型的数学能力，靠的是竞赛题和基准集，题目都有标准答案，做对做错一目了然；这次面对的是一个没人知道答案的开放问题，交出来的是一份要送同行审阅的稿子。当评价标准从"答对没有"换成"审稿人认不认"，能力的天花板在哪儿，暂时谁也说不准。