新智元報(bào)道編輯：編輯部 HYZ
【新智元導(dǎo)讀】最近，大家都被這條消息嚇到了：傳說(shuō)Grok 3已經(jīng)成功證明出黎曼猜想？！雖然這是在玩梗，但還是讓我們來(lái)仔細(xì)剖析下，目前的AI距離千禧年數(shù)學(xué)難題，究竟還有多遠(yuǎn)。
黎曼猜想，竟被Grok 3「證明」了？
為此，xAI暫停了Grok 3的訓(xùn)練來(lái)驗(yàn)證它的證明，如果結(jié)果是正確的，將會(huì)完全終止模型的訓(xùn)練。
xAI工程師Hieu Pham在社交媒體的最新「爆料」，成為AI圈最火爆的話題。
要知道，黎曼猜想是千禧年七大數(shù)學(xué)難題之一，被譽(yù)為「猜想界的皇冠」。
2000年，黎曼猜想被美國(guó)克雷數(shù)學(xué)研究所（Clay Mathematics Institute of Cambridge，CMI）指定為「七大千禧年難題之一」
由于信息量太大，網(wǎng)友們直接被整懵了，分不清這是真的還是在玩梗……
幾個(gè)小時(shí)之后，在Pham另一個(gè)帖子中，證明了這只是自己的調(diào)侃。
惡搞的起因是，一位網(wǎng)友Andrew Curran最先「爆料」，傳言稱Grok3在訓(xùn)練時(shí)發(fā)生了災(zāi)難性事件。
明眼的網(wǎng)友很快便質(zhì)疑道：LLM訓(xùn)練怎么會(huì)出現(xiàn)災(zāi)難性事件？
即便是出現(xiàn)loss激增，也只需要回到上一個(gè)Checkpoint，調(diào)整一下，就可以接著訓(xùn)了。
除非是服務(wù)器全燒了，數(shù)據(jù)全都不剩了……
眼瞧著消息越傳越廣，xAI聯(lián)創(chuàng)Greg Yang坐不住了。
對(duì)此，他用諷刺的語(yǔ)氣調(diào)侃道：「對(duì)對(duì)對(duì)，Grok 3訓(xùn)著訓(xùn)著突然開(kāi)始攻擊辦公室的保安了�！�
另一位研究人員Heinrich Kuttler也接梗道：「對(duì)對(duì)對(duì)，情況非常糟糕！我們后來(lái)用nan（Not a Number，非數(shù)）把所有壞的權(quán)重都替換了一遍，才恢復(fù)。」
網(wǎng)友見(jiàn)狀，也跟著玩起了梗。
要攻克黎曼猜想，還差些什么？
言歸正傳，讓我們來(lái)仔細(xì)看一下，目前人類離攻克黎曼猜想還差幾步。
如今，「黎曼猜想」就像是一座巍峨的高峰，165年來(lái)從未有人成功攀上。
它就像大海中的燈塔，為數(shù)學(xué)領(lǐng)域的發(fā)展指明方向：很多數(shù)論和復(fù)變函數(shù)領(lǐng)域的工作都基于黎曼猜想為真這個(gè)前提，因此一旦證明了黎曼猜想，許多其他工作也會(huì)得到完整的證明。
黎曼猜想起源于德國(guó)數(shù)學(xué)家高斯，他給出了一個(gè)公式，能夠近似地預(yù)測(cè)出任意數(shù)字的素?cái)?shù)個(gè)數(shù)。
在1859年，德國(guó)數(shù)學(xué)家波恩哈德黎曼改進(jìn)了高斯的公式，用涉及復(fù)變量函數(shù)演算的方法，得出一個(gè)原創(chuàng)公式。
這就是赫赫有名的「黎曼猜想」。
根據(jù)公式，能夠畫(huà)出無(wú)窮多個(gè)點(diǎn)。黎曼猜測(cè)，這些點(diǎn)有一定的排列規(guī)律，一部分在一條橫線上，另一部分則在一條豎線上，所有點(diǎn)都在兩條直線上排列，無(wú)一例外。
黎曼ζ函數(shù)可視化
理論上，無(wú)法證明是否所有的點(diǎn)都在這兩條線上，但是，只要有一個(gè)點(diǎn)不在，就能推翻黎曼猜想！
現(xiàn)在，數(shù)學(xué)家們已經(jīng)用計(jì)算機(jī)驗(yàn)證了最初的15億個(gè)點(diǎn)，全部符合黎曼猜想。
雖然是一個(gè)弱一點(diǎn)的形式，但本質(zhì)上已經(jīng)是解決了朗道西格爾零點(diǎn)問(wèn)題。
論文鏈接：https://arxiv.org/abs/2211.02515
論文地址：https://arxiv.org/abs/2405.20552
當(dāng)然，盡管我們離完全解決這一猜想還很遙遠(yuǎn)。
AI的數(shù)學(xué)能力，到底什么水平？
這么說(shuō)起來(lái)，目前的AI是否真的有證明黎曼猜想的能力呢？
我們可以來(lái)看看，爆火全網(wǎng)的AI證明工具AlphaProof，是如何做出IMO 2024的三道題的。
從某種角度來(lái)說(shuō)，IMO數(shù)學(xué)競(jìng)賽題跟「猜想界的皇冠」黎曼猜想距離有多遠(yuǎn)，那離AI證明黎曼猜想也就有多遠(yuǎn)。
谷歌DeepMind研究人員，AlphaProof負(fù)責(zé)人Rishi Mehta最新博客中，介紹了AlphaProof在IMO中的最新表現(xiàn)。
4個(gè)月前，谷歌DeepMind團(tuán)隊(duì)發(fā)布了兩個(gè)數(shù)學(xué)推理新模型AlphaProof和AlphaGeometry 2。
前者在破解IMO 2024六道競(jìng)賽試題中，做對(duì)了其中4道，而且每道題拿下了滿分，相當(dāng)于銀牌選手水平（28分）。
而在最新進(jìn)展文章中，Mehta揭示了AlphaProof在IMO 2024解題中最酷的想法。
在證明過(guò)程中，AlphaProof會(huì)使用Lean 生成證明，并且每個(gè)Lean證明由一系列策略組成。
因此，Mehta將挑選出對(duì)應(yīng)于這些想法的策略，針對(duì)AlphaProof解決的第 1、2和6題進(jìn)行分析。
問(wèn)題 1
問(wèn)題
確定所有實(shí)數(shù)α，使得對(duì)于每一個(gè)正整數(shù)n，整數(shù)α+2α++nα是n的倍數(shù)。（注意，z表示小于或等于z的最大整數(shù)。例如，π=4 和2=2.9=2。）
解答
答案是所有偶整數(shù)。
需要注意的是，AlphaProof解決這些問(wèn)題的方式是，提出許多解答候選者，嘗試證明和反駁每一個(gè)，最終僅為正確答案找到證明。
這里看到的證明是，證明答案是偶整數(shù)集的那個(gè)。
證明偶整數(shù)滿足給定性質(zhì)顯而易見(jiàn)，而這個(gè)證明的難點(diǎn)在于，證明除了偶整數(shù)之外沒(méi)有其他α能夠滿足它。
AlphaProof以一種有趣（盡管復(fù)雜）的方式做到這一點(diǎn)：
它首先設(shè)定一個(gè)整數(shù)，使得 2=α+2α。這是成立的，因?yàn)橥ㄟ^(guò)將n=2代入給定性質(zhì)，便可知道右側(cè)是偶數(shù)。
existsλx L=>(L 2 two_pos).rec λl Y=>?_
L 2是在n=2的情況下使用給定性質(zhì)。此外，AlphaProof經(jīng)常將幾個(gè)策略組合在一行中。一個(gè)更易理解的版本是：
constructor intro x Lobtain l, Y := L 2 (by exact two_pos)
注意，我們還將α重命名為x。接下來(lái)，它聲稱（并繼續(xù)證明）對(duì)于所有自然數(shù) n，(n+1)α=α+2n(α) ……（1）.
suffices: (n : ),(n+1)*x = x+2 * ↑ (n : ) * (l-((x)))
從中，它能夠得到α=2(α)。
use(l-x)*2
這必須是一個(gè)偶整數(shù)（因?yàn)樗且粋�(gè)整數(shù)乘以 2）。
它證明這些事情的方式涉及一些相當(dāng)復(fù)雜的簡(jiǎn)化。但設(shè)置（1）中的聲明是使其余證明成立的令人印象深刻的一步。
Mehta稱，對(duì)我來(lái)說(shuō)，這一聲明的動(dòng)機(jī)相當(dāng)不直觀，而事實(shí)上一切都能奏效幾乎是神奇的。
AlphaProof的完整解決方案如下：
上下滑動(dòng)查看
問(wèn)題 2
問(wèn)題
找到所有滿足條件的正整數(shù)對(duì)(a,b)，使得存在正整數(shù)g和N，使得gcd(an+b,bn+a)=g對(duì)于所有整數(shù)n≥N成立。
解答
AlphaProof正確給出 (1,1) 是唯一的解。
為了證明沒(méi)有其他解可以成立，它要求我們考慮數(shù)ab+1。它聲稱（并隨后證明）ab+1必須整除g。
suffices:b.1*b.2+1Y
需要注意的是，AlphaProof決定將對(duì) (a,b) 重命名為b，以便它必須將元素引用為b.1和b.2。出于某種原因，它還選擇將變量g重命名為 Y。
現(xiàn)在，選擇n=N(ab+1)，可以得到(ab+1)(aN(ab+1)+b) 和 (ab+1)(bN(ab+1)+a)。
由于ab+1與a和b互質(zhì)，因此可以應(yīng)用歐拉定理，即
a(ab+1)≡1(modab+1)
b(ab+1)≡1(modab+1)
所以有ab+11+b和ab+11+a，由此可以得出a=b=1。
這一策略緊密地遵循了人類對(duì)此問(wèn)題的證明。選擇考慮ab+1是構(gòu)建證明的巧妙想法。
AlphaProof 的完整解決方案如下：
上下滑動(dòng)查看
問(wèn)題 6
問(wèn)題
設(shè)Q是所有有理數(shù)的集合。一個(gè)函數(shù)f:Q→Q被稱為aquaesulian函數(shù)，如果對(duì)于每個(gè)x,y∈Q，滿足以下性質(zhì)：f(x+f(y))=f(x)+y或f(f(x)+y)=x+f(y)。
證明存在一個(gè)整數(shù)c，使得對(duì)于任何aquaesulian函數(shù)f，形式為f(r)+f(r)的有理數(shù)最多有c個(gè)不同的值，并找出c的最小可能值。
解答
AlphaProof求解答案為c=2，證明過(guò)程分為兩部分。
首先，它通過(guò)證明f(r)+f(r)只能是0或某個(gè)單一的其他值來(lái)證明c≤2。這部分證明相當(dāng)復(fù)雜，并巧妙地利用了給定的aquaesulian性質(zhì)。
完成這一步后，c可以是1或2。
為了證明 c=2，AlphaProof提出了一個(gè)aquaesulian函數(shù) f(x)=x+2x，使得 f(r)+f(r)取兩個(gè)不同的值。
specialize V $ λ N=>-N+2 *Int.ceil N
然后它展示了f(1)+f(1)=0和f(1/2)+f(1/2)=2，這給出了需要的兩個(gè)不同的值。
useFinset.one_lt_card.2$byexists@0,V.1.mem_toFinset.2(byexists-1),2,V.1.mem_toFinset.2(byexists1/2)
再次，很多內(nèi)容被壓縮到一行中，但通過(guò)exists -1和 exists 1/2展示了兩個(gè)不同的值。
這是一個(gè)值得注意的函數(shù)構(gòu)造，而且相當(dāng)難以找到！在509名參與者中只有5人解決了 P6，值得注意的是Tim Gowers在評(píng)審這個(gè)解決方案時(shí)也嘗試了一下，但沒(méi)有找到一個(gè)能給出兩個(gè)不同值的函數(shù)。
畢竟，IMO 2024第六題被稱為「終極boss」，可不是那么輕易就解決掉的。
AlphaProof的完整解決方案如下：
上下滑動(dòng)查看
