AI面对黎曼猜想：它还会在哪些地方绊倒

摘要 黎曼猜想（RH）被普遍视为数学史上最重要的悬而未决难题之一。一个半世纪过去，它依旧让所有证明路线无功而返。随着人工智能逐步走入数学推理：能解竞赛题、能做复杂定理的检验、甚至能生成新的猜想——一个顺理成章的追问出现了：AI有没有可能证明黎曼猜想？若有，又需要满足哪些前提？要回答它，我们不得不正视当下AI的短板、数学发现究竟依赖什么、形式化验证在其中扮演的作用，以及在证明能够被“认证”为无误之前必须搭建的巨型知识支架。下面将从三个互相缠绕的方向拆解：当前AI欠缺的关键能力、把解析数论搬进形式系统的浩大工