摘要
黎曼猜想仍然是数学中最重要的未解问题之一。我们并不声称已找到证明，而是探讨一个可验证的AI辅助推理系统是否能够产生可靠的、经过形式检查的部分进展，并明确识别剩余的数学障碍。我们将可验证的渐进物理变换器与递归自我改进（VGPT-RSI）应用于两个与RH相邻的认证任务。
首先，我们构建并验证了一个在参数化安全下限曲线上的有限RH边界证书。该数值边界曲线被转换为一个有证书支持的下限曲线，通过外向取整区间算术和Arb/FLINT球算术进行审核，然后在Rocq/CoqInterval中检查该参数化定理。
其次，我们启动了一个正式的Lagarias路线证书。Lagarias标准表明，RH等价于全局不等式。我们形式化了有限数量并生成了一个Coq检查的有限证书。最终系统识别出确切的未解决数学瓶颈：形式化Lagarias等价性、证明全局尾定理超出任何有限截止，以及可能将反例减少到极其丰盛或相关的极端整数。
这些结果表明，VGPT-RSI能够产生经过认证的与RH相邻的正式进展，组织证明依赖关系，并在剩余障碍确实是数学问题时避免过度声称。
博主点评： 该研究展示了利用AI辅助的形式验证方法在解决复杂数学问题中的潜力，尤其是黎曼猜想这一重要课题。通过构建边界证书和明确未解障碍，VGPT-RSI为进一步的数学探索提供了新的思路与工具。它不仅推动了形式化数学的发展，也为AI在数学领域的应用提供了有力的实例。