AI 中文总结
该研究无条件证明黎曼ζ函数至少三分之二非平凡零点为单零点且位于临界线，六分之五为不同零点，采用Montgomery-Taylor窗后精度提升，结果可推广至本原Dirichlet L-函数且在Lean 4中完成形式验证。
AI 中文摘要
我们无条件证明，按重数计数的黎曼ζ函数非平凡零点中，至少三分之二是单零点且位于临界线上，至少六分之五是不同的零点；此前的无条件记录为5/12和0.6603。采用Montgomery-Taylor窗后，这些常数变为0.6725和0.8362。该论证使Montgomery在1973年的推导成为无条件：原本用于将零点侧解读为实纵坐标正和的黎曼假设，被应用于Weil厄米型有限压缩的秩-迹不等式取代，利用Sylvester惯性定律处理离线零点对。分析输入来自Aryan，以及Baluyot、Goldston、Suriajaya和Turnage-Butterbaugh的工作。该结果可推广至本原Dirichlet L-函数，且已在Lean 4中完成形式验证。
英文摘要
We prove unconditionally that at least two thirds of the nontrivial zeros of the Riemann zeta function, counted with multiplicity, are simple and lie on the critical line, and that at least five sixths are distinct; the previous unconditional records are $\frac{5}{12}$ and $0.6603$. With the Montgomery--Taylor window the constants become $0.6725$ and $0.8362$. The argument makes Montgomery's 1973 deduction unconditional: the Riemann hypothesis, classically needed to read the zero side as a positive sum over real ordinates, is replaced by a rank-trace inequality applied to a finite compression of Weil's Hermitian form, with Sylvester's law of inertia handling off-line pairs. The analytic inputs are those of Aryan and of Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh. The results extend to primitive Dirichlet $L$-functions and are formally verified in Lean 4.
Comments21 pages. Proof discovered autonomously by Claude (Anthropic); verified and communicated by the listed authors. See §1 for provenance. Lean formalization available
