Riemann zeta函数的零点中超过83.69%是互不相同的
More than 83.69% of the zeros of the Riemann zeta function are distinct
浏览论文内容
中文总结 AI 辅助
本文通过引入带自由裁剪参数的矩阵不等式，将Riemann zeta函数互异非平凡零点的下渐近比例从0.83625提升至0.83699，并在Lean 4中形式化证明，展示了AI辅助数学研究的潜力。
中文摘要 AI 辅助
Riemann zeta函数的互不相同的非平凡零点（按重数计数）的下渐近比例至少为$0.8369928814\ldots$。此前的界为$0.83625\ldots$。与证明该界的方法相同，Montgomery对关联定理的一个无条件版本给出了渐近能量估计。新的要素是一个带有自由裁剪参数的短矩阵不等式。它加强了用互不相同的零点数目表示的能量下界。其增益来自临界线上不同邻近零点之间重叠的非负修正，即使其中某些零点是二重的，该修正仍然保留。矩阵不等式、阈值引理、分块二分法、计数组装和精确算术均在Lean 4中形式化证明。该常数依赖于近期工作中一个计算机辅助的局部不等式，该工作尚未经过评审。该计算被独立重新运行，并且所有导入的输入均已列出。本文主要是一次AI辅助数学研究的实验（第4节）。
英文摘要
The lower asymptotic proportion of distinct nontrivial zeros of the Riemann zeta function, relative to the total number counted with multiplicity, is at least $0.8369928814\ldots$. Earlier work proves $0.83625\ldots$, and a report we have not verified claims $0.83672\ldots$. As in the proof of the bound $0.83625$, an unconditional version of Montgomery's pair-correlation theorem gives an asymptotic energy estimate. The new ingredient is a short matrix inequality with a free clipping parameter. It strengthens the lower bound for this energy in terms of the number of distinct zeros. The gain is a nonnegative correction from overlaps between different nearby zeros on the critical line, which is retained even when some of these zeros are double. The matrix inequality, the threshold lemma, the block dichotomy, the counting assembly and the exact arithmetic are proved formally in Lean 4. The constant relies on a computer-assisted local inequality from recent work that has not yet been refereed. That computation was re-run independently, and every imported input is listed. This paper is primarily an experiment in AI-assisted mathematical research (Section 4).
