新智元报道编辑：编辑部 HYZ
【新智元导读】最近，大家都被这条消息吓到了：传说Grok 3已经成功证明出黎曼猜想？！虽然这是在玩梗，但还是让我们来仔细剖析下，目前的AI距离千禧年数学难题，究竟还有多远。
黎曼猜想，竟被Grok 3「证明」了？
为此，xAI暂停了Grok 3的训练来验证它的证明，如果结果是正确的，将会完全终止模型的训练。
xAI工程师Hieu Pham在社交媒体的最新「爆料」，成为AI圈最火爆的话题。
要知道，黎曼猜想是千禧年七大数学难题之一，被誉为「猜想界的皇冠」。
2000年，黎曼猜想被美国克雷数学研究所（Clay Mathematics Institute of Cambridge，CMI）指定为「七大千禧年难题之一」
由于信息量太大，网友们直接被整懵了，分不清这是真的还是在玩梗……
几个小时之后，在Pham另一个帖子中，证明了这只是自己的调侃。
恶搞的起因是，一位网友Andrew Curran最先「爆料」，传言称Grok3在训练时发生了灾难性事件。
明眼的网友很快便质疑道：LLM训练怎么会出现灾难性事件？
即便是出现loss激增，也只需要回到上一个Checkpoint，调整一下，就可以接着训了。
除非是服务器全烧了，数据全都不剩了……
眼瞧着消息越传越广，xAI联创Greg Yang坐不住了。
对此，他用讽刺的语气调侃道：「对对对，Grok 3训着训着突然开始攻击办公室的保安了。」
另一位研究人员Heinrich Kuttler也接梗道：「对对对，情况非常糟糕！我们后来用nan（Not a Number，非数）把所有坏的权重都替换了一遍，才恢复。」
网友见状，也跟着玩起了梗。
要攻克黎曼猜想，还差些什么？
言归正传，让我们来仔细看一下，目前人类离攻克黎曼猜想还差几步。
如今，「黎曼猜想」就像是一座巍峨的高峰，165年来从未有人成功攀上。
它就像大海中的灯塔，为数学领域的发展指明方向：很多数论和复变函数领域的工作都基于黎曼猜想为真这个前提，因此一旦证明了黎曼猜想，许多其他工作也会得到完整的证明。
黎曼猜想起源于德国数学家高斯，他给出了一个公式，能够近似地预测出任意数字的素数个数。
在1859年，德国数学家波恩哈德黎曼改进了高斯的公式，用涉及复变量函数演算的方法，得出一个原创公式。
这就是赫赫有名的「黎曼猜想」。
根据公式，能够画出无穷多个点。黎曼猜测，这些点有一定的排列规律，一部分在一条横线上，另一部分则在一条竖线上，所有点都在两条直线上排列，无一例外。
黎曼ζ函数可视化
理论上，无法证明是否所有的点都在这两条线上，但是，只要有一个点不在，就能推翻黎曼猜想！
现在，数学家们已经用计算机验证了最初的15亿个点，全部符合黎曼猜想。
虽然是一个弱一点的形式，但本质上已经是解决了朗道西格尔零点问题。
论文链接：https://arxiv.org/abs/2211.02515
论文地址：https://arxiv.org/abs/2405.20552
当然，尽管我们离完全解决这一猜想还很遥远。
AI的数学能力，到底什么水平？
这么说起来，目前的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题进行分析。
问题 1
问题
确定所有实数α，使得对于每一个正整数n，整数α+2α++nα是n的倍数。（注意，z表示小于或等于z的最大整数。例如，π=4 和2=2.9=2。）
解答
答案是所有偶整数。
需要注意的是，AlphaProof解决这些问题的方式是，提出许多解答候选者，尝试证明和反驳每一个，最终仅为正确答案找到证明。
这里看到的证明是，证明答案是偶整数集的那个。
证明偶整数满足给定性质显而易见，而这个证明的难点在于，证明除了偶整数之外没有其他α能够满足它。
AlphaProof以一种有趣（尽管复杂）的方式做到这一点：
它首先设定一个整数，使得 2=α+2α。这是成立的，因为通过将n=2代入给定性质，便可知道右侧是偶数。
existsλx L=>(L 2 two_pos).rec λl Y=>?_
L 2是在n=2的情况下使用给定性质。此外，AlphaProof经常将几个策略组合在一行中。一个更易理解的版本是：
constructor intro x Lobtain l, Y := L 2 (by exact two_pos)
注意，我们还将α重命名为x。接下来，它声称（并继续证明）对于所有自然数 n，(n+1)α=α+2n(α) ……（1）.
suffices: (n : ),(n+1)*x = x+2 * ↑ (n : ) * (l-((x)))
从中，它能够得到α=2(α)。
use(l-x)*2
这必须是一个偶整数（因为它是一个整数乘以 2）。
它证明这些事情的方式涉及一些相当复杂的简化。但设置（1）中的声明是使其余证明成立的令人印象深刻的一步。
Mehta称，对我来说，这一声明的动机相当不直观，而事实上一切都能奏效几乎是神奇的。
AlphaProof的完整解决方案如下：
上下滑动查看
问题 2
问题
找到所有满足条件的正整数对(a,b)，使得存在正整数g和N，使得gcd(an+b,bn+a)=g对于所有整数n≥N成立。
解答
AlphaProof正确给出 (1,1) 是唯一的解。
为了证明没有其他解可以成立，它要求我们考虑数ab+1。它声称（并随后证明）ab+1必须整除g。
suffices:b.1*b.2+1Y
需要注意的是，AlphaProof决定将对 (a,b) 重命名为b，以便它必须将元素引用为b.1和b.2。出于某种原因，它还选择将变量g重命名为 Y。
现在，选择n=N(ab+1)，可以得到(ab+1)(aN(ab+1)+b) 和 (ab+1)(bN(ab+1)+a)。
由于ab+1与a和b互质，因此可以应用欧拉定理，即
a(ab+1)≡1(modab+1)
b(ab+1)≡1(modab+1)
所以有ab+11+b和ab+11+a，由此可以得出a=b=1。
这一策略紧密地遵循了人类对此问题的证明。选择考虑ab+1是构建证明的巧妙想法。
AlphaProof 的完整解决方案如下：
上下滑动查看
问题 6
问题
设Q是所有有理数的集合。一个函数f:Q→Q被称为aquaesulian函数，如果对于每个x,y∈Q，满足以下性质：f(x+f(y))=f(x)+y或f(f(x)+y)=x+f(y)。
证明存在一个整数c，使得对于任何aquaesulian函数f，形式为f(r)+f(r)的有理数最多有c个不同的值，并找出c的最小可能值。
解答
AlphaProof求解答案为c=2，证明过程分为两部分。
首先，它通过证明f(r)+f(r)只能是0或某个单一的其他值来证明c≤2。这部分证明相当复杂，并巧妙地利用了给定的aquaesulian性质。
完成这一步后，c可以是1或2。
为了证明 c=2，AlphaProof提出了一个aquaesulian函数 f(x)=x+2x，使得 f(r)+f(r)取两个不同的值。
specialize V $ λ N=>-N+2 *Int.ceil N
然后它展示了f(1)+f(1)=0和f(1/2)+f(1/2)=2，这给出了需要的两个不同的值。
useFinset.one_lt_card.2$byexists@0,V.1.mem_toFinset.2(byexists-1),2,V.1.mem_toFinset.2(byexists1/2)
再次，很多内容被压缩到一行中，但通过exists -1和 exists 1/2展示了两个不同的值。
这是一个值得注意的函数构造，而且相当难以找到！在509名参与者中只有5人解决了 P6，值得注意的是Tim Gowers在评审这个解决方案时也尝试了一下，但没有找到一个能给出两个不同值的函数。
毕竟，IMO 2024第六题被称为「终极boss」，可不是那么轻易就解决掉的。
AlphaProof的完整解决方案如下：
上下滑动查看
