AI破解千禧年难题传闻背后：数学的“金蛋”与黑箱危机

【科技纵览】当顶尖数学家丘成桐被曝出悬赏十万元，征集对庞加莱猜想证明的形式化验证时，这一举动意外揭开了AI介入基础科学研究的深层焦虑。此前，清华姚班校友彭天翼利用Claude系统完成费马大定理形式化的消息刚引发热议，网络上便流传起另一则更为惊人的传闻：Anthropic的Claude可能已攻克纳维-斯托克斯（N-S）方程，甚至涉及其他千禧年大奖难题。尽管克莱数学研究所截至9月6日仍将N-S方程列为未解状态，且所有信源均指向OpenAI员工的二手转述，缺乏独立一手证据，但这场关于AI数学能力的讨论已远超技术本身。

陶哲轩对此保持审慎态度，他坦言AI解决此类难题“并非完全不可能”，但随即抛出更深刻的忧虑：若AI以黑箱方式给出答案，数学探索过程中催生的工具与直觉将被彻底锁死。以N-S方程为例，数十年来数学家在求解中建立的Leray-Hopf弱解理论等基础设施，其价值远超答案本身；正如费马大定理的证明推动了模形式理论的发展，这些猜想如同“下金蛋的鸡”。陶哲轩警告，若AI仅为了刷榜而暴力求解，可能杀死这只鸡，导致数学领域停止生长。他甚至构建了一个反事实思想实验：假如2005年就有AI暴力求解素数间距问题，张益唐的突破及随之诞生的梅纳德筛法可能被埋没，整个领域的演进轨迹将被改写。

然而，商业巨头的步伐并未因伦理担忧而放缓。2026年的AI数学军备竞赛已进入白热化阶段。Anthropic在未发布的研究模型上尝试证明黎曼猜想，虽未成功，却将零点满足猜想的比例下界提升至67.2%，打破人类纪录；驱动这一突破的员工Jarred Sumner并无数学背景，仅靠提示词不断试错。与此同时，OpenAI宣布Astra解决了十个悬而未决十年的数学难题，包括构造非sofic群，全部附带Lean 4形式化证明，算力成本仅约2000美元。谷歌DeepMind的AlphaProof Nexus也在同期证明了多个Erdos开放问题。

值得注意的是，AI生成的证明文件规模正迅速超出人类理解的极限。Claude在11天内完成的费马大定理形式化包含1300万行代码和60亿Token输出，伦敦帝国理工的Kevin Buzzard评价其为“非凡成就”，但人类验证已退化为运行编译器检查报错。这种趋势预示着ASI（人工超级智能）降临的前兆：当推理过程变成无法解读的黑箱，人类在科学探索中积累的直觉模式可能在物理意义上失效。预测市场Manifold显示，“2026年AI解决千禧年大奖难题”的合约报价已达38%。对于寻求万亿级IPO估值的科技巨头而言，解决百年数学难题不仅是技术验证，更是赋予公司“神迹感”的关键背书。Goodhart定律再次应验：当指标成为唯一目标，度量价值的意义便随之消解。在这场速度与深度的博弈中，凡人终将被甩在身后，而数学的未来形态，或许将在黑箱与光明的夹缝中重塑。