用AI验证系统推进黎曼猜想邻近问题,明确标出未解数学瓶颈。
VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization
- 用递归自改进的AI系统生成可形式化验证的边界证书
- 在参数化区域上构建并证明有限形式不等式,精度达区间算术要求
- 精准定位三大数学障碍,适合形式化验证与数论研究者参考
黎曼猜想仍是数学中最重要的未解难题之一。本文不宣称证明,而是探索可验证的AI辅助推理系统能否产生可靠的形式化部分进展,并明确标识剩余数学障碍。我们应用具备递归自改进能力的可验证生长物理变换器(VGPT-RSI)于两个黎曼猜想邻近的认证任务。首先,构造并验证了一个关于参数化安全下界曲线的有限黎曼猜想边界证书。数值边界曲线经向外舍入区间算术与Arb/FLINT球算术转换为证书支撑的下界曲线,并在Rocq/CoqInterval中完成参数化定理的形式化检查。其次,启动形式化拉加里亚路径证书:拉加里亚准则指出黎曼猜想等价于全局不等式。我们形式化了有限量并生成了Coq验证的有限证书。最终系统精确识别出未解数学瓶颈:形式化拉加里亚等价性、在任意有限截断外证明全局尾部定理,以及将反例归约为高度合数或相关极值整数的可能性。结果表明,VGPT-RSI可生成可信的黎曼猜想邻近形式进展,组织证明依赖关系,并在真实数学障碍面前避免过度宣称。
原文摘要 · Abstract (English)
The Riemann Hypothesis remains one of the central unsolved problems in mathematics. Rather than claiming proof, we investigate whether a verifiable AI-assisted reasoning system can produce reliable, formally checked partial progress while explicitly identifying the remaining mathematical obstructions. We apply the Verifiable Growing Physical Transformer with Recursive Self-Improvement (VGPT-RSI) to two RH-adjacent certification tasks. First, we construct and verify a finite RH-boundary certificate for inequality on a parameterized safe lower curve over a region. The numerical boundary curve is converted into a certificate-backed lower curve, audited using outward-rounded interval arithmetic and Arb/FLINT ball arithmetic, and then checked in Rocq/CoqInterval for the parameterized theorem. Second, we initiate a formal Lagarias-route certificate. Lagarias criterion states that RH is equivalent to the global inequality. We formalize the finite quantity and produce a Coq-checked finite certificate. The final system identifies the exact unresolved mathematical bottlenecks: formalizing the Lagarias equivalence, proving the global tail theorem beyond any finite cutoff, and potentially reducing counterexamples to colossally abundant or related extremal integers. These results demonstrate that VGPT-RSI can produce certified RH-adjacent formal progress, organize proof dependencies, and avoid overclaiming when the remaining obstruction is genuinely mathematical.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。