🤖 人工智能 · 数学研究

🔥 从IMO银牌到推翻八十年猜想，AI正在从"解题工具"进化成"证明伙伴"，但距离独立攻克黎曼猜想级别的难题，仍差一次真正的思想跃迁。

一、AI 已能"证明"什么级别的数学猜想

把时间拨回2024年，DeepMind 的 AlphaProof 在IMO（国际数学奥林匹克）中解出多道压轴题，达到银牌水准，那是AI首次在奥赛赛场拿到奖牌级表现。而到了2026年，这层窗户纸被彻底捅破：OpenAI 一个内部通用推理模型，自主推翻了埃尔德什1946年提出的"单位距离猜想"，这个困扰几何界整整八十年的经典难题就此告破。

更关键的是，这份证明并非暴力搜索，而是从代数数论的"无限类域塔""Golod-Shafarevich理论"里搬来了看起来毫不相干的工具，用全新构造方式给出反例。菲尔兹奖得主蒂莫西·高尔斯直言："以前没有任何AI生成的证明能接近这个水准。"这背后透露的信号是：AI不仅能解有答案的题，已经开始触碰"开放问题"这个数学研究的核心地带。

二、能力有，但"证明"与"验证"是两回事

要回答"能不能证明猜想"，得先分清三个层次：解奥赛题、形式化已知证明、独立攻克开放猜想——三者的证据强度天差地别。OpenAI 这次突破虽然惊艳，但最终仍请了9位顶级数学家人工复核，还大幅改写了证明让它更简洁。换句话说，AI自己还无法确证自己没犯错。

谷歌的做法则更激进：AlphaProof Nexus 用 Lean 形式化语言让编译器逐行检查推理，理论上摆脱了对人工质检的依赖，一口气解决9道埃尔德什难题，单题成本最低仅7.5美元。但中科院数学机械化实验室的实践也暴露出短板——自然语言证明能力与形式化证明能力之间存在巨大鸿沟，多数AI生成的证明仍需要专家来兜底验证。

三、真正还差的那一步是什么

正如北大教授刘若川那句耐人寻味的话："AI能穷尽迷宫的每个角落，但只有人类能决定飞越迷宫。"现阶段AI的"证明"，更像是把人类已知知识的凸包补得更满，而不是在未知方向上探索得更远。它没有学科壁垒、没有权威偏见，敢推翻八十年共识，这种"大力出奇迹"令人敬畏，却还难以提出黎曼猜想级别的根本性新方向。

所以结论很清晰：AI已经具备了证明"著名数学猜想"的真实能力，2026年的成果就是铁证；但这种能力目前更接近"强力助手"而非"独立研究者"，人机协作仍是主流。当形式化验证基建真正成熟、当模型学会主动定义"好问题"的那一天，那个"飞越迷宫"的起点，才会真正到来。

综合OpenAI官方博客、DeepMind研究成果、中科院数学机械化实验室及36氪报道 | 2026年8月