AI 辅助数论研究把 Riemann ζ 函数不同零点比例下界提升到 83.699%

Kristian Muri Knausgård 报告将 Riemann ζ 函数不同非平凡零点的下渐近比例下界从约 0.83625 提升到 0.8369928814。新证明使用带自由截断参数的矩阵不等式强化能量下界，关键矩阵不等式、threshold lemma、block dichotomy、counting assembly 和精确算术均在 Lean 4 中形式化。论文明确称这项工作‘主要是一次 AI-assisted mathematical research 实验’，同时保留一个来自近期工作的 computer-assisted local inequality 输入，该输入尚未经过正式同行评审。