ainta 独立复现确认 Claude 黎曼 zeta 证明：至少 67.25% 零点为单零点且在临界线上

8 月 11 日，独立研究者 ainta 在 X 上确认，Anthropic 由 Claude 撰写的黎曼 zeta 论文证明了"至少 67.25% 的零点为单零点且位于临界线上"，并公开了复现仓库；他把论文交给 GPT-5.6-Sol Pro 后，下界被进一步推到 67.30%。当天 23:37（UTC），确认，Anthropic 为这一结果准备的 Lean 形式化证明通过了 Comparator 校验。

8 月 10 日，Anthropic 在中公布了这一结果：未发布的研究版 Claude 把黎曼 zeta 函数满足黎曼猜想的零点比例下界从 41.6% 提高到 67.2%，博客同时称 Claude 与 Anthropic 员工 Eric Easley 合作产出了一份可校验的形式化证明。

ainta 复现确认 67.25%，GPT-5.6-Sol Pro 给出 67.30085%

8 月 11 日 04:41（UTC），账号写道："Anthropic published a paper today, written by Claude, proving that at least 67.25% of the zeros of the Riemann zeta function are simple and on the critical line."

他的 X 简介标注为 QED_Audit 研究员、IOI 金牌、两届 ICPC World Finals 金牌（第 2、第 3 名），现为密码学博士生。截至抓取，这条帖子显示 110 万次浏览、2040 个赞、107 次转发。

帖子第二句交代了 67.30% 的来源："I gave Claude's paper to GPT-5.6-Sol Pro. It's now 67.30%."他链接的于 8 月 11 日创建，README 说明这是对 Claude 论文《More Than Two Thirds of the Zeros of the Riemann Zeta Function Lie on the Critical Line》（）中 Theorem D 的扩展，附完整证明与可复现的有限验证。论文 Theorem D 的原下界是 liminf N₀ˢ(T,2T)/N(T,2T) ≥ 3/2 − (1/√2)cot(1/√2) = 0.672500703679…，即 67.25%。

仓库在 Theorem D 之上加了两条新论证：取 3 个连续零点时得到 ε₄ ≥ 221/10⁶，对应下界 67.2519767%；取 7 个连续零点时得到一个六变量下界 ≥ 19/5000，对应 67.3008528%。主结果写为 liminf ≥ 0.673008527927…。

验证器使用 Arb 区间算术和穷举细分，运行 zeta-zero-verify three 与 zeta-zero-verify seven 即可重跑，每次从公式重建全部超越数包络。仓库状态栏写的是："Research draft generated by GPT-5.6 Sol. Independent verification and peer review are welcome."这条 67.30% 扩展是 GPT-5.6 Sol 生成的研究草稿，作者自己写明欢迎独立验证与同行评审。

Lean 官方确认：形式化证明通过 Comparator

8 月 11 日 23:37（UTC），发帖："Great to see that these results include not only a Lean formalization, but one that passes validation in Comparator."帖子同时附上了仓库。

仓库于 8 月 6 日创建，是对论文 Theorems A–E 的完整 Lean 4/Mathlib 形式化，不含 sorry。所有解析输入都有证明：Weil 显式公式、Riemann–von Mangoldt 零点计数、Γ′/Γ 的 Stirling 型估计、Chebyshev–Mertens 素数估计、Montgomery–Vaughan 广义 Hilbert 不等式。

顶层定理没有假设，仓库不声明任何公理，#print axioms 只报告 propext、Classical.choice、Quot.sound 三条标准公理。Theorem D 的 0.67250 下界以 ≥ 2 − 1/c₁* 的形式收录其中（c₁* = √2·tan ϑ/(1+ϑ·tan ϑ)，ϑ = 1/√2）。

Comparator 指仓库的 comparator/ 目录：15+12+6 条受信任的题目声明配上解，最强的检查是语句相等性核对加 Lean 内核重放证明。仓库标注为研究产物、不维护、不接受贡献，主要贡献者账号 eeeasley 对应博客中提到的 Eric Easley。截至抓取，仓库有 45 颗星；Lean 官方这条帖子显示约 7254 次浏览。

67.2% 是博客口径，67.25% 是定理常数，67.30% 还在等评审

67.2% 是 Anthropic 博客给出的数字，论文 Theorem D 的精确常数是 0.672500703679…，即 ainta 复现确认的 67.25%。两者是同一个定理。

"单零点且在临界线上"比"在临界线上"更强：N₀ˢ 只数临界线上互不相同的单零点，N 数的是带重数的全部零点。ainta 仓库的主结果写为 liminf N₀ˢ(T,2T)/N(T,2T) ≥ 0.673008527927…。

67.30% 是三者中唯一尚未经同行评审的一环：它来自 ainta 仓库对 Theorem D 的扩展，仓库明确标注草稿由 GPT-5.6 Sol 生成。Anthropic 的 Lean 形式化覆盖论文原定理（含 0.67250 下界），不含 ainta 仓库的这条 67.30085% 扩展。

黎曼猜想本身仍然没有被证明

Anthropic 在里写明了边界："We don't expect that the techniques Claude used will lead to proving the Riemann hypothesis."公司不认为这套技术路径能最终证明黎曼猜想。

博客还披露，Anthropic 的数学家 Levent Alpöge 与 Ralph Furman 验证了论文，Brian Conrey 与 Dan Goldston 两位该领域专家在短时间内审阅了论文。实验发起者、Anthropic 员工 Jarred Sumner 在 8 月 10 日的里写的是个人评价："Still not sure what that means, but some analytic number theorists seem excited."

目前公开可核验的进展停在两处：论文的 67.25% 下界有通过 Comparator 的 Lean 形式化与 ainta 的独立复核；67.30085% 的扩展仍是等待同行评审的研究草稿。

参考链接

ainta 的确认帖：
ainta 的复现仓库：
Lean 官方确认帖：
Anthropic 的 Lean 形式化仓库：
Anthropic 研究博客：
论文 PDF：
Jarred Sumner 的帖子：