【新智元导读】最近，关于Grok 3成功证明黎曼猜想的消息在社交媒体上引起了热议。虽然这被证实是玩梗，但让我们仔细探讨下，目前AI距离解决千禧年数学难题还有多远。

黎曼猜想，竟被Grok 3「证明」了？ xAI暂停了Grok 3的训练来验证其证明，如果结果正确，将终止模型训练。xAI工程师Hieu Pham在社交媒体上的“爆料”成为AI圈最火的话题。

要知道，黎曼猜想是千禧年七大数学难题之一，被誉为“猜想界的皇冠”。

几个小时后，Pham在另一帖子中澄清，这只是自己的调侃。恶搞的起因是一位网友的“爆料”，称Grok3在训练时出现了灾难性事件。

要攻克黎曼猜想，还差些什么？ 言归正传，我们来看，人类距离攻克黎曼猜想还有多远。黎曼猜想就像是一座巍峨的高峰，165年来无人攀上。它就像大海中的灯塔，为数学领域的发展指明方向。黎曼猜想源于德国数学家高斯，他给出了一个公式，能够近似地预测出任意数字的素数个数。在1859年，德国数学家波恩哈德·黎曼改进了高斯的公式，用涉及复变量函数演算的方法，得出一个原创公式。这就是赫赫有名的“黎曼猜想”。

理论上，无法证明是否所有的点都在两条直线上，但只要有一个点不在，就能推翻黎曼猜想。现在，数学家们已经用计算机验证了最初的15亿个点，全部符合黎曼猜想。

2022年，张益唐发表111页论文，宣布本质上已证明朗道-西格尔零点问题——广义黎曼猜想的一种特殊且弱得多的形式。用他的话说，关于零点猜想问题，“大海里的针我没捞到，但海底地貌我探得差不多了”。

2024年，陶哲轩力推MIT数学教授Larry Guth和牛津大学菲尔兹奖得主James Maynard的一篇新论文，认为两人在证明黎曼猜想方面取得了重大突破。

AI的数学能力，到底什么水平？ 那么，目前的AI是否真的有证明黎曼猜想的能力呢？我们来看看AlphaProof在IMO 2024中的表现。从某种程度上说，IMO数学竞赛题与“猜想界的皇冠”黎曼猜想有多远，那离AI证明黎曼猜想也就有多远。

谷歌DeepMind研究人员，AlphaProof负责人Rishi Mehta在博客中介绍了AlphaProof在IMO中的最新表现。4个月前，谷歌DeepMind团队发布了两个数学推理新模型AlphaProof和AlphaGeometry 2。前者在破解IMO 2024六道竞赛试题中，做对了其中4道，而且每道题拿下了满分，相当于银牌选手水平（28分）。

而在最新进展文章中，Mehta揭示了AlphaProof在IMO 2024解题中最酷的想法。在证明过程中，AlphaProof会使用到Lean生成证明，并且每个Lean证明由一系列策略组成。因此，Mehta挑选出对应于这些想法的策略，针对AlphaProof解决的第1、2和6题进行分析。

AI距离千禧年难题，还有多远？ 关于AI究竟能做什么程度的数学题，网友们展开了讨论。很多人认为，数学将是AI最先突破的领域之一，因为存在一个可用的既便宜又快速的反馈循环。数学具有这样的特性：你可以以很少的成本，100%去验证你所做的事是否正确。

不过，有一名数学家在评论区现身说法，认为并不值得用AI这么做。在他看来，计算时间/成本与问题复杂性之间的权衡，值得严肃考虑。理论上讲，用形式语言找到证明是一件很轻松的事，因为只需一直搜索可能的证明，直到找到所需陈述结尾的证明就可以了。

而如果进一步设想，现在的Alphaproof如果变成具有天文数字计算资源的定理证明器，我们或许有一天就可以证明“P/NP问题”。因为，任何可证明的定理，都可以通过耐心地使用穷举法，列举所有可能的证明来找到。

离AI解决P/NP问题、黎曼猜想这样的千禧年难题，还会有多远呢？马斯克曾许诺，用10万块H100训练的Grok 3将在年底发布，应该会令人惊叹。而如今，这个规模已经扩展到了20万台，再给一点时间，说不定Grok 3真能出奇迹。