AI证明数学猜想：丘成桐悬赏十万，陶哲轩警示黑箱风险

近日，著名数学家丘成桐悬赏10万元，征集佩雷尔曼庞加莱猜想证明的形式化验证。此前，清华姚班校友彭天翼基于Claude的Prove2Me系统，首次形式化证明了费马大定理。庞加莱猜想指出，封闭三维空间中每条封闭曲线若能收缩成一点，则该空间同胚于三维球面，2006年数学界认可了佩雷尔曼的证明。

传闻与回应

与此同时，一则传闻在数学界与AI圈激起涟漪：Anthropic的Claude已解决千禧年难题纳维-斯托克斯（N-S）方程，证明正送专家评审。该方向也是数学家韦东奕的主攻领域。若属实，Claude内部模型的数学推理能力将远超公开版本。对此，菲尔兹奖得主陶哲轩回应称，AI攻克此类难题“并非完全不可能”，但若以黑箱方式解决，可能弊大于利。

陶哲轩的洞见

陶哲轩的核心观点是：著名猜想的价值在于求解过程催生的工具，答案本身次要。AI以黑箱给出答案，将锁死过程中的洞见，问题虽在技术上被解决，但数学却停止生长。他以N-S方程为例，指出求解催生了Leray-Hopf弱解理论等奠基性工具；费马大定理的求证则催生了模形式理论。AI的暴力证明，如同“拿走蛋却杀死下金蛋的鸡”。他同时举出Erdős problem #1026作为正面案例，并批评那些不与专家合作、不提交评审、只为刷基准分数的做法。

现状与竞赛

截至9月6日，克雷数学研究所仍将N-S方程列为未解问题。所有传闻信源可追溯至OpenAI员工的转述，并无独立一手来源。陶哲轩也承认，即便理想解决，最终构造也将极其复杂，人类无法仅凭自身验证。9月4日，Claude完成了费马大定理的Lean形式化：1300万行代码，29500条中间定理，60亿Token输出，人类验证已退化为运行编译器检查是否报错。

2026年的AI数学军备竞赛已然展开：8月，Anthropic未发布模型尝试证明黎曼猜想未果，但将零点比例下界从41.6%推至67.2%；OpenAI Astra解决了10个悬而未决至少十年的问题，包括首次构造非sofic群，总成本约2000美元；谷歌DeepMind AlphaProof Nexus解决了9个Erdős开放问题。预测市场显示，“2026年AI解决千禧年难题”的概率约为18%。分析指出，Anthropic和OpenAI需证明实现ASI以支撑万亿美元级IPO估值，而解决纯数学难题最能赋予“神迹感”。

这场由AI掀起的数学革命，既带来突破的曙光，也引发对学科本质的深思。陶哲轩的警示，如同悬在狂热之上的清醒剂：当AI能轻易给出答案，人类数学家或许更需珍视探索过程中的每一步。丘成桐的悬赏，则是对形式化验证这一新范式的有力推动。未来，AI与数学家能否携手共进，而非彼此替代，将决定数学这门古老学科的下一个篇章。