AI 中文总结
本研究通过计算机辅助不等式与Lean 4形式化证明，改进了黎曼zeta函数零点分布的下界：超过83.9%的零点互异，超过67.35%为临界线上的简单零点，并给出相应上界。
AI 中文摘要
设N(T)计数黎曼zeta函数在高度T以内的非平凡零点（计入重数），N_d(T)为互不相同零点的个数，N_0^s(T)为位于临界线上的简单零点个数。我们证明liminf N_d(T)/N(T) ≥ 1645064/1960733 = 0.83900...；此前工作证明了0.83699...，而一份我们尚未验证的报告声称0.83805...。因此，超过67.80%的零点是简单的。此外，liminf N_0^s(T)/N(T) ≥ 0.67353...；此前工作证明了0.67250...，而我们尚未验证的报告声称0.673492。Lamzouri的两个估计被改进：至少88.93%的零点为简单零点或位于临界线上，且简单零点与临界线上零点的比例平均至少为83.67%。根据Montgomery对关联定理的无条件形式，能量（即测试函数在零点对上的求和）渐近已知。一个重数为d的零点对其贡献d^2，而邻近的零点也有贡献，因此对这类零点对的能量下界限制了多重零点可用的能量。证明分三步。首先，对于间隔至少为平均间距固定比例的零点，大筛不等式允许其零点对（计入重数）被完整使用。其次，其贡献通过一个计算机辅助不等式给出下界，该不等式针对七个或八个连续零点，区分简单零点和二重零点，其修正项作为存储函数的增量而相消。第三，选择测试函数以在能量代价下最大化此贡献。我们还证明了对于两个主要测试函数，此类不等式所能达到的上限。下界与这些上限均在Lean 4中证明，包括解析输入。证明使用了Mathlib之外的三个公理，每个不等式一个。每个公理记录了一个搜索程序返回真；Lean的内核不检查运行本身。这项工作是对AI辅助数学研究的实验。
英文摘要
Let N(T) count the nontrivial zeros of the Riemann zeta function up to height T with multiplicity, N_d(T) the distinct ones, and N_0^s(T) those that are simple and on the critical line. We prove liminf N_d(T)/N(T) >= 1645064/1960733 = 0.83900...; earlier work proves 0.83699..., and a report we have not verified claims 0.83805.... Hence more than 67.80% are simple. Also liminf N_0^s(T)/N(T) >= 0.67353...; earlier work proves 0.67250..., and reports we have not verified claim 0.673492. Two estimates of Lamzouri are improved: at least 88.93% of the zeros are simple or on the critical line, and the proportions of simple zeros and of zeros on the line average at least 83.67%. By the unconditional form of Montgomery's pair-correlation theorem the energy, a sum of a test function over pairs of zeros, is known asymptotically. A zero of multiplicity d contributes d^2 to it and nearby zeros contribute too, so a lower bound for such pairs leaves less energy for multiple zeros. The proof has three steps. First, for zeros at least a fixed fraction of the mean spacing apart, a large sieve inequality lets their pairs be used in full, with multiplicities. Second, their contribution is bounded below by a computer-assisted inequality for seven or eight consecutive zeros which distinguishes simple and double zeros. Its correction terms telescope, as increments of a storage function. Third, the test function is chosen to make this contribution large, at the cost of more energy. We also prove upper limits for what such inequalities can give with the two main test functions. The lower bounds and these limits are proved in Lean 4, analytic inputs included. The proofs use three axioms beyond those of Mathlib, one per inequality. Each records that a search program returned true; Lean's kernel does not check the run itself. This work is an experiment in AI-assisted mathematical research.
Comments43 pages, 3 figures, 13 tables. Lean 4 proofs, certificate data and source code are in the ancillary files and at https://github.com/kristianmk/839
