Claude 把零点比例下界推至 67.25%：科研智能体的分水岭不是会做题，而是能否交付可审计的新知识

2026-08-11

一、触发新闻与一句话定义

Anthropic 在 2026 年 8 月 10 日公布，未发布的研究版 Claude 在尝试黎曼猜想时，把可无条件证明位于临界线上的黎曼 ζ 函数零点比例下界从 41.6% 提高到 67.25%，并给出论文、Lean 形式化证明与完整研究过程记录。 两轮 Claude Code 会话共生成约 3,100 万输出 Token；第二轮持续一天半，由约 60 个 Claude 子智能体运行 2,400 次 Shell 命令、编写数百个 Python 脚本并做数千次数值检查。Anthropic 的两位内部数学家 Levent Alpöge 和 Ralph Furman 审阅了结果，长期研究 ζ 函数零点的 Brian Conrey 与 Dan Goldston 也在短时间内检查了论文；截至发布日，该结果尚未经历传统期刊同行评审。

这里的研究对象，不只是一个百分比，而是一种新的科研生产系统：通用模型在长时程中并行生成路线、用代码和文献淘汰错误、让相互隔离的实例做敌对审稿，再把幸存论证交给形式证明器和人类专家复核。

先把最容易误读的一点钉牢。67.25% 是渐近意义上的无条件下界：当高度趋向无穷时，至少这一比例的非平凡零点可证明是简单零点且位于临界线。它不是“已经检查了 67.25% 的零点”，也不是“黎曼猜想完成了 67.25%”。论文明确说，这套工具对黎曼猜想本身没有正反方向的直接推进；哪怕某种密度结论达到 100%，仍可能容许稀疏的线外零点。更关键的是，论文给出自身路线的天花板：只利用带宽 1 的配对相关信息时，认证上限约为 68.185%。从 67.25% 走向 100%，不是再多跑几轮智能体就能补齐的 32.75 个百分点，而是需要新的数学信息。

二、纵向分析：从诞生到当下

1859—1973：一个关于素数的问题，逐渐变成“零点在哪里”

1859 年，黎曼在研究素数计数时引入 ζ 函数，并猜测它的所有非平凡零点都落在实部为 1/2 的临界线上。零点的位置控制素数分布误差的细致程度，所以这条看似几何的竖线，后来成了数论中最有名的边界之一。

完整证明太难，数学家先问一个弱一些、但仍然精确的问题：至少有多少比例的零点能证明在临界线上？

1914 年，G. H. Hardy 证明临界线上有无穷多个零点。1942 年，Atle Selberg 证明有一个正比例的零点在临界线上，但没有给出漂亮的显式常数。1974 年，Norman Levinson 用“mollifier”方法把比例推到三分之一。这个方法可以粗略理解为：给 ζ 函数乘上一个精心设计的短 Dirichlet 多项式，抵消它在临界线附近的剧烈波动，再通过均值估计数出足够多的零点。此后几十年，比例下界的每次提高都沿着这条路精修。

1989 年，Brian Conrey 把下界推过 40%。Bui、Conrey、Young，Feng，以及 Pratt、Robles、Zaharescu、Zeindler 继续改进 mollifier 的形状、长度和矩估计，到 2020 年将纪录推到 5/12，也就是 41.666…%。从 Levinson 的 1/3 到 5/12，46 年只增加了 8.33 个百分点。进展缓慢，不是因为没人计算，而是每一次改进都要控制更长的多项式、更复杂的交叉项，以及当前数论工具暂时触不到的素数相关结构。

这条纵轴解释了为什么 67.25% 会显得突兀：它没有把原有 mollifier 再拧紧一点，而是换了赛道。

1973—2026：另一条路一直卡在“正性”

在 Levinson 方法成形的前一年，Hugh Montgomery 提出了 ζ 零点的配对相关方法。他把零点间距的统计与素数侧的和式联系起来；在假设黎曼猜想成立时，这套方法能证明至少三分之二的零点是简单零点。后来 Montgomery–Taylor 的优化把条件性常数推到约 0.6725，Cheer–Goldston 等工作又在更强信息下继续提高。

这里有一个尴尬的结构：素数一侧的二阶矩计算本来是无条件的，真正依赖黎曼猜想的是零点一侧的读法。若所有零点都在同一条直线上，每个贡献可以按非负实数处理；一旦允许零点离线，贡献变成带正负方向的厄米型，逐项正性消失，经典计数步骤就断了。

近年的 Baluyot、Goldston、Suriajaya、Turnage-Butterbaugh 等人把这个障碍剥得更清楚。他们证明 Montgomery 的 form factor 可以无条件地对所有复零点求和；Goldston 与 Suriajaya 又说明，如果额外假设全部零点挤在临界线附近一个足够窄的竖盒里，就能无条件恢复三分之二结论。他们在论文中直接追问：能不能从 Montgomery 的证明里移除黎曼猜想？

到这里，问题已不再是“算不出素数侧”，而是“怎样读取一个不再正定的零点侧”。Claude 的贡献，正好落在这个接口。

2000 年埋下的工具：不要逐项数，改看整个空间的惯性

Enrico Bombieri 在 2000 年讨论过 Weil 判据与黎曼猜想的关系。Weil 的显式公式可以被写成测试函数空间上的厄米型；如果这个型在整个空间上正定，便等价于黎曼猜想。若存在离线零点，厄米型会出现负方向。

传统做法倾向于逐个读零点贡献。Claude 换了视角：把无限维对象压缩到一个有限维测试函数族，得到 Gram 矩阵，然后不再要求矩阵逐项为正，而是研究它有多少正特征值、多少负特征值以及秩有多大。

临界线上的一个不同零点贡献一个非负的秩一方向；由函数方程配对的线外零点则贡献一个符号为 (1,1) 的块，也就是一个正方向加一个负方向。Sylvester 惯性定律保证这种正负方向的数量在合适变换下不乱跑。再把矩阵的迹、Frobenius 范数和正惯性指数放进一个秩—迹不等式，便能从 Montgomery 的一阶、二阶矩反推出：必须有足够多的正方向来自临界线上的零点，而不能全由线外成对零点“冒充”。

论文的核心不是某个巨大公式，而是一次表示方式的转换：过去缺失的逐项正性，被整个矩阵的惯性结构替代。用标准窗口得到 2/3；优化测试函数后，常数变成 0.67250…，恰好恢复 Montgomery–Taylor 在黎曼猜想成立条件下得到的常数，但现在不需要假设黎曼猜想。

同一论证还给出两个附带结果：至少 67.25% 的零点是简单且位于临界线上；至少 83.625% 的零点彼此不同。论文也将主要结论扩展到固定的本原 Dirichlet L 函数。

2023—2025：AI 数学先学会“在封闭规则里赢”

Claude 的这次结果并非凭空发生。过去三年，AI 数学沿着两条路径演进。

第一条是形式优先。Google DeepMind 的 AlphaGeometry 把语言模型用于提出辅助构造，再让符号演绎引擎完成可检查的几何证明。它用一亿个合成样本训练，在 30 道奥数几何题中解出 25 道，接近人类金牌选手平均水平。2024 年，AlphaProof 把预训练模型与 AlphaZero 式强化学习接入 Lean，和 AlphaGeometry 2 一起在当年 IMO 得到 28/42 分，达到银牌上沿。它们证明了一件很重要的事：只要问题被翻译进规则完备、反馈明确的形式环境，机器可以用大规模搜索和学习找到人类不容易发现的证明路线。

代价也很清楚。2024 年的 IMO 题目需要人工翻译成形式语言；部分题目耗时最多三天；系统主要处理已知有答案、边界明确的竞赛题。它擅长的是“给定形式命题，找一条内核接受的路径”，尚未覆盖开放研究中的选题、文献定位、错误命题识别和结果解释。

第二条是通用模型与人类专家共研。2025 年，OpenAI 披露 GPT-5 在组合数学、优化、物理和生物学中的案例：模型高速提出变体、借用邻近领域工具，人类研究者负责识别有效方向、补齐论证并承担发表责任。Ernest Ryu 用 GPT-5 在约 12 小时内推进一个 40 年开放问题，但模型给出的若干论证也有错误，且无法独自组装完整证明。另一项案例中，GPT-5 给出一个漂亮结论，后来才发现同样的结果和证明早已发表，暴露出“重新发现”与“真正发现”之间的文献归因风险。

到 2026 年 2 月，OpenAI 的 First Proof 实验让内部模型尝试十道研究级问题。官方认为至少五份答案很可能正确，但也公开撤回了对第 2 题正确性的早期判断。这个细节比成功率更有价值：研究数学没有自动排行榜，模型写完并不等于任务结束，专家审阅本身就是计算链条的一部分。

2026 年 8 月：一次失败任务，怎样侧向长出新定理

Anthropic 最初给 Claude 的任务并不保守。员工 Jarred Sumner 让一个未发布研究模型“认真尝试”黎曼猜想。第一轮，Claude 生成并试验了 650 个想法，没有一个成功。若按聊天机器人的使用习惯，故事到这里就该结束：模型回答“这是未解难题”，用户关闭窗口。

第二轮改变的不是问题，而是工作制度。Claude 用一天半协调约 60 个子智能体：2 个负责发展关键数学思想，13 个向它们供给候选路线，30 个探索新想法但未成功，13 个专门验证，最后 2 个协助写初稿。它们调用 Shell 2,400 次，写了数百个 Python 脚本，对已知 ζ 零点做数千次数值检查，还下载 54 篇 arXiv 论文排查优先权。

成功路线最初也不是奔着“比例下界”去的。一个编号 E2 的子智能体想给 Weil 厄米型的负惯性指数找上界，结果发现这条路给不出东西；它反过来看正方向，先得到“至少一半零点在线上”的候选结论。Claude 自己的第一反应是怀疑，因为这已经超过停滞多年的 5/12。

系统没有让提出结论的实例自己反复说服自己，而是把不同接缝拆给三个相互隔离的敌对审稿者：一个检查窗口外零点是否泄漏进有限维压缩，一个检查素数侧是否偷用了黎曼猜想或 Hardy–Littlewood 级别的输入，一个检查线外零点的 (1,1) 块与线性代数。它还把同一管线运行在类黎曼猜想为假的 Davenport–Heilbronn 与 Epstein 函数上做“证明过头”测试。第四个审稿者处理边界、渐近误差和 Gram 矩阵条件数。

一半不是终点。另一子智能体把 Cauchy–Schwarz 的粗计数升级为经 von Neumann 迹不等式推出的秩—迹不等式，利用线外块不只是“占一个正方向”，还必须同时占一个负方向，比例由 1/2 跳到 2/3。两个盲审实例从头重证核心引理，系统又在 10 万个随机矩阵和数百个对抗优化样本上寻找反例。数值测试不构成证明，但它适合在正式证明前快速击穿符号、归一化和边界错误。

最后一道门才是人。Alpöge 与 Furman 把结果放回解析数论文献中，Conrey 与 Goldston 在短时间内检查论文；Eric Easley 协调 Claude 生成 Lean 4 形式化。公开仓库将计数函数直接定义在 Mathlib 的 riemannZeta 上，顶层定理没有额外假设，项目声明无 sorry，公理审计只显示 Lean/Mathlib 常用的三项标准公理。代码、固定工具链、比较器配置、论文和过程记录一起发布，使第三方至少拥有复算和挑错的入口。

这次跃迁真正积累了什么

纵向看，67.25% 由三种积累叠加而来。

第一层是人类数学积累。Hardy、Selberg、Levinson、Conrey 与后续作者建立了比例问题；Montgomery 给出配对相关框架；Bombieri揭示 Weil 型的惯性视角；BGSTB 与 Goldston—Suriajaya把“条件到底藏在哪里”剥离出来。Claude 没有绕开这些工作，而是重新组合了它们。

第二层是机器工作流积累。代码智能体已经学会在文件系统、终端、论文库和测试框架之间移动；多智能体让探索与审稿并行；长时间运行把一次回答变成持续实验。31 万、310 万还是 3,100 万 Token，并不会自动产生定理，但足够的计算预算使大量失败可以被记录、比较和主动终止。

第三层是验证基础设施。没有 Mathlib、Lean 内核、公开零点数据和可复现脚本，模型的长篇证明仍然只是一个高风险文本对象。形式化并不是文章末尾的装饰，而是把“相信哪个模型”改成“检查哪个命题、依赖哪些公理、代码能否通过内核”。

这三层缺一不可。把功劳全归给模型，会抹掉百余年数学和开源形式化社区；把它仅仅称为自动补全，又解释不了为什么人类长期没有把这些已知部件接成同一个无条件论证。

三、横向分析：竞争图谱

当前 AI 数学不是一场单一排行榜，而是四种生产方式的竞争。

Google DeepMind：先把数学变成可判定的游戏

AlphaGeometry 和 AlphaProof 的优势来自历史选择：它们先缩小世界，再在其中做到极强。几何系统把“下一步加哪条辅助线”交给神经模型，把推导交给规则引擎；AlphaProof 直接在 Lean 中用强化学习搜索。每一步都有清晰反馈，错误路径很快归零，训练可以使用海量合成题。

这种路线的用户体验接近一台强大的定理证明机。用户愿意付出的前置成本是形式化：定义必须进入库，题意必须准确翻译，缺失引理要先补。回报是输出一旦被内核接受，就不会在普通推理步骤上含糊其辞。

它的生态位是“验证密集、边界清楚”的数学。竞赛题、已有库覆盖良好的代数和组合问题很适合；像黎曼零点比例这样需要决定读哪些论文、发现旧框架的缺口、做数值探路并重写研究问题的任务，单纯的形式搜索很难独立承担。Claude 此次不是在 Lean 内搜索出整个发现，而是先用自然语言、文献和矩阵实验找到论证，随后才形式化。两者不是替代关系，更像发现端与证明端的不同排序。

OpenAI：Astra 已把竞争推到“批量新结果 + Lean 证书”

OpenAI 的早期路线更接近现实中的数学合作。GPT-5 不要求问题先完全形式化，它能读自然语言、跨领域调用定理、提出构造或反例。Ryu 的案例显示，它最有价值的能力不是一次写出漂亮终稿，而是让研究者用极高频率试错：多数路线失败，但失败成本从数天压缩到几分钟。

这条路线把人类放在回路中心。专家决定问题怎样切、哪个模型建议值得追、何时另开会话隔离错误，以及最终论文如何表述。优势是能进入文献还没被形式化的专业领域；弱点也来自同一点：自然语言没有自动裁判。First Proof 中一份最初被看好的答案后来被判错，说明“多采样 + 人工挑最佳”仍可能放大确认偏误。GPT-5 重新发现已发表结果却未主动归因，则说明新颖性核查不能交给同一段生成链。

2026 年 5 月，OpenAI 又公布内部模型对 Erdős 平面单位距离猜想的反例；8 月 1 日，未发布的 Astra 一次发布十项数学与理论计算机结果，覆盖高维球堆积、非 sofic 群、算术电路、量子并行重复、格密码和 Ramsey 数等领域。OpenAI 称找到这十项解法的 Token 按 Sol API 价格折算约 2,000 美元，人类与模型共同整理稿件，随后由模型为每项论证生成 Lean 证书。

这使 Astra 成为 Claude 此次最直接的横向参照：两者都是闭源研究模型，都从开放的自然语言问题出发，也都把论文、推理说明和 Lean 工件作为交付物。差别在可见的组织过程。Anthropic 披露了约 60 个角色化子智能体、失败路线、Shell 调用和敌对复核；OpenAI 披露了结果组合与成功运行的价格口径，却没有同等详细地说明总共尝试多少问题、失败花费多少、是否采用多智能体。仅看成功样本，Astra 的单位成本更低、领域覆盖更广；仅看审计链，Claude 的研究过程更透明。

Claude 与 OpenAI 共享“通用模型做发散搜索”的长处，但把人类专家的部分职责拆成了机器角色：提出者、反例寻找者、文献审计者、盲重证者各自隔离。区别暂时不宜归结为某个模型更会数学，而应落在两个可测变量上：每项新结果消耗多少总计算，以及证据链让外部专家多快找到错误。

Gemini/Aletheia 与开放研究代理：从一道名题转向批量问题组合

2026 年出现的另一类系统试图把开放数学规模化。Aletheia 报告在约 700 个 Erdős 问题上做半自主评估，并给出若干开放问题的解答；其他结合 Lean 的代理在数百个 Erdős 问题和 OEIS 猜想上批量运行。它们的核心想法是：科研突破不一定来自所有算力押在一个世纪难题，也可能来自系统性扫描“注意力不足”的问题库，把可解的小岛先捞出来。

这类系统的优势是吞吐量和公开问题基准，风险是数据库状态。一个标为 open 的问题可能已有冷门论文解决，或者原命题在不同文献中使用了不同限定。OpenAI 的归因失误已经说明，找到证明与确认新颖是两项任务。Anthropic 本次让独立子智能体下载 54 篇论文排查先例，正是在补这个洞；但搜索不到先例仍不等于先例不存在。

与批量扫描相比，黎曼 ζ 事件更像“深井模式”：60 个代理、3,100 万输出 Token、一天半都围绕一个高度拥挤的问题域。它证明模型不只会收割注意力不足的低垂果实，也可能把一个成熟子领域中彼此熟悉却未连接的部件接起来。代价是单位结果的计算、审稿和沟通成本远高于批量筛查。

开源 Lean 生态：真正的共同底座，不是第五家模型公司

横向比较很容易只盯着 Anthropic、Google 和 OpenAI，却忽略所有路线共同借力的 Mathlib、Lean 与学术开源库。AlphaProof 在 Lean 中训练；研究代理用 Lean 编译器作反馈；Claude 的结论靠 Lean 仓库提供可复核承诺。竞争发生在模型层，可信度却越来越依赖一个共享的、不是由单一模型公司拥有的证明层。

对数学用户而言，这个分工很现实。模型可以闭源，推理轨迹可以昂贵，最终命题和证明对象仍应尽量开放。Anthropic 公开了静态 Lean 工件、Apache 2.0 许可、固定 Mathlib 提交和审计步骤，这是本次结果比一条社交媒体“模型解决名题”更强的原因。但仓库发布当天几乎没有外部使用记录，且工具链采用候选版本；真正的可复现性要等第三方在不同环境里完成构建、逐项核对形式命题与论文命题的一致性。

谁占据了什么位置

Google 当前最强的护城河是形式环境中的训练和搜索；OpenAI 已用 Astra 抢占“跨领域批量新结果 + Lean 证书”，并用约 2,000 美元的成功运行口径压低成本预期；Aletheia 和开放代理押注批量、半自治的研究流水线；Anthropic 此次最突出的信号，则是把“从开放目标到新结果，再到敌对复核和完整证据包”的过程披露得更细。

这个位置很诱人，也最容易被一次错误击穿。竞赛成绩错一道题，只损失几分；开放数学论文若核心定义错配、优先权判断失误或形式化证明的命题比自然语言声称的弱，整个行业信号都会反转。所以横向竞争最终不会只比“谁先宣布突破”，而会比三项速度：发现速度、第三方理解速度、独立推翻错误的速度。

四、横纵交汇洞察

判断一：突破来自换表示，不来自把旧路线算得更久

纵轴上，41.6% 是 Levinson—Conrey 路线几十年优化的结果；横轴上，当前模型最擅长大规模尝试和跨文献重组。两条线交汇后，可以看清这次突破为何发生：Claude 没有继续优化 mollifier，而是把 Montgomery 的配对相关、Bombieri 的惯性观察和近期无条件 form factor 结果放进同一矩阵框架。

我的判断是，科研智能体近期最有价值的能力不是凭空发明全新数学语言，而是发现“同一个对象在不同子领域里被写成了不同表示”。人类专家深耕一个方向时，会自然继承该方向的标准表示；模型同时读大量相邻文献，更容易尝试不合传统的接口。此次从逐项正性转向矩阵惯性，就是这种接口型创新。

这也解释了它的边界。表示转换能绕开一个旧瓶颈，却不会消灭信息论天花板。论文自己算出，带宽 1 数据最多认证约 68.185%。模型已经把这条路走到离天花板不到 1 个百分点的位置。若后续版本只是把 67.25% 调到 67.8%，那是同一路线的精修；只有获得更宽 Fourier 支撑的配对相关信息、引入新的素数相关估计，或找到不依赖这组矩的证书，才算进入下一阶段。

判断二：多智能体的价值不在“人多”，而在制度化的不信任

60 个子智能体是最显眼的数字，却不是最关键的设计。若 60 个实例共享同一上下文、共同追随一个漂亮结论，它们只会形成高速共识。此次系统有效的地方，是给角色加上冲突：发现者不能兼任唯一审稿者；不同审稿者各查一个具体失效模式；盲重证实例看不到原推导；反例测试使用已知类比命题为假的控制对象。

历史上，数学共同体靠同行评审、研讨班和后续论文实现这种不信任，周期以月和年计算。Claude 把其中一部分压缩到一天半。但机器审稿不能替代共同体，因为同源模型可能共享训练盲点，60 个实例也不是 60 个独立认识主体。它更像提交前的高强度内部审计：能清除大量低级和中级错误，提高交给人类专家的候选质量，却不能自行授予“已被数学界接受”的身份。

因此，真正可迁移到材料科学、药物发现或金融模型研究的，不是“开 60 个 Agent”，而是为每类主张预先指定失败模式：数据泄漏由谁查，基线错配由谁查，因果方向由谁查，外推边界由谁查，已有工作由谁查。科研智能体的组织结构，正在成为与模型参数同样重要的实验变量。

判断三：形式证明把可信度从品牌迁到工件，但没有消灭语义风险

纵向上，AI 数学从 AlphaGeometry 的专用验证、AlphaProof 的 Lean 内搜索，走到 Claude 的自然语言发现后验形式化；横向上，各家都在向可检查输出靠拢。方向很清楚：未来一项 AI 数学声明的最小交付物，不应只有论文 PDF，而应包括形式命题、固定依赖、可构建证明、过程记录和优先权搜索日志。

Lean 能保证“这些形式命题由这些公理推出”，却不能单独保证形式命题就是读者以为的自然语言命题，也不能判断结果是否新、是否重要。Claude 仓库直接使用 Mathlib 的 ζ 函数并公开计数定义，已经主动压缩了语义错位空间；第三方仍需检查零点重数、极限量词、dyadic 区间与累计计数等定义是否完全对应论文叙述。

这是一种新的学术分工：内核负责逻辑，人类负责语义与价值，检索系统负责优先权，智能体负责探索。过去一篇论文把这些工作揉在作者和审稿人身上；现在它们可以被拆开、记录并分别复算。

判断四：Anthropic 的优势和包袱来自同一个选择——把 Claude Code 变成实验室操作系统

Claude 此次优势可以追溯到代码智能体的工程积累。文件系统、Shell、Python、并行任务、长会话和文档生成原本服务软件开发，搬进数学后正好承接文献下载、数值试验、证明版本管理和形式化构建。Claude Code 不是报告里的外围工具，它是让通用模型从“会答数学题”变成“能维持研究状态”的容器。

包袱也在这里。3,100 万输出 Token 和大量并行实例说明该流程昂贵；未发布模型使外部团队无法做同条件对照；提示鼓励似乎改变了模型是否持续探索，说明行为仍对实验者互动敏感；过程日志虽然公开，但要完整阅读和重放的成本极高。若只有模型公司内部能承担这种实验，开放数学可能出现新的算力门槛。

Anthropic 当前最该证明的不是再挑一座名题制造头条，而是同一流程能否在预注册问题集上稳定产出：总共尝试多少题，多少为真正新结果，多少被人类否决，平均成本多少，第三方复核要多久。单个惊艳样本说明能力存在，不能说明能力可靠。

三个未来剧本

最可能的剧本：可审计的“机器博士后”先普及。 未来 12—24 个月，通用模型不会稳定解决千禧年难题，但会大量承担文献拼接、反例搜索、计算实验、引理生成和形式化迁移。顶尖数学家把它当作不疲倦、知识面宽但需要严厉管理的合作者。论文开始附带 Agent 日志、Lean/Coq 工件和模型贡献说明。最先受益的是问题定义清楚、验证成本低于发现成本的组合数学、数论、优化和理论计算机科学。

最危险的剧本：宣布速度超过消化速度。 模型公司连续发布高难度候选结果，内部模型互审被包装成独立验证，外部数学家来不及重建证明。少数错误或优先权事故让公众在“AI 已接管数学”和“全是营销”之间摆动。真正的风险不是某一篇错稿，而是审稿注意力被海量机器论文耗尽，谁拥有算力谁就能把验证成本外包给公共学术共同体。

最乐观的剧本：发现层与证明层形成开放协议。 各家模型可以闭源竞争，但结果以统一、可构建的形式工件交付；问题库记录状态、版本和先例；第三方证明器和不同模型交叉重证；计算预算、失败路线和人类干预被标准化披露。此时数学家不必相信 Anthropic、OpenAI 或 Google，只需检查对象。AI 不只是更快地产生论文，而是让“一个结果为什么可信”比今天更透明。

黎曼 1859 年留下的是一句“非常可能”，之后一百多年，数学的工作就是把可能性一点点变成可证明的陈述。Claude 这次没有完成那句猜想，却把科研智能体也推到了同一条纪律上：想法可以大胆，结论必须留下别人能够独立检查的路。

67.25% 最值得记住的地方，不是它看起来离 100% 更近，而是它第一次较完整地展示了这种路可以由机器参与铺设。

五、信息来源

1. Anthropic：Learning more about Claude's mathematical capabilities 2. Claude / Anthropic：More Than Two Thirds of the Zeros of the Riemann Zeta Function Lie on the Critical Line（论文 PDF） 3. Anthropic GitHub：zeta-23-lean 形式化证明仓库 4. NIST Digital Library of Mathematical Functions：Riemann Zeta Function — Zeros 5. Pratt、Robles、Zaharescu、Zeindler：More than five-twelfths of the zeros of ζ are on the critical line 6. Feng：Zeros of the Riemann zeta function on the critical line 7. Goldston、Suriajaya：Zeta Zeros on the Critical Line 8. Baluyot、Goldston、Suriajaya、Turnage-Butterbaugh：Pair correlation of zeros of the Riemann zeta-function 9. Google DeepMind：AlphaGeometry — An Olympiad-level AI system for geometry 10. Google DeepMind：AlphaProof and AlphaGeometry 2 achieve silver-medal standard at IMO 2024 11. Nature：Olympiad-level formal mathematical reasoning with reinforcement learning 12. OpenAI：Early experiments in accelerating science with GPT-5 13. OpenAI：How GPT-5 helped mathematician Ernest Ryu solve a 40-year-old open problem 14. OpenAI：Our First Proof submissions 15. OpenAI：An OpenAI model has disproved a central conjecture in discrete geometry 16. OpenAI：Ten advances in mathematics and theoretical computer science 17. Feng 等：Towards Autonomous Mathematics Research 18. Tsoukalas 等：Advancing Mathematics Research with AI-Driven Formal Proof Search 19. Achim 等：Aristotle — IMO-level Automated Theorem Proving 20. Anthropic：Zeta 研究的发现过程与详细说明 21. Anthropic：Zeta 研究关键子智能体记录 22. Anthropic GitHub：zeta-23-lean 审计记录 23. Lean 社区：Lean Theorem Prover