黎曼猜想，竟被Grok 3「證明」了？

為此，xAI暫停了Grok 3的訓(xùn)練來驗(yàn)證它的證明，如果結(jié)果是正確的，將會(huì)完全終止模型的訓(xùn)練。

xAI工程師Hieu Pham在社交媒體的最新「爆料」，成為AI圈最火爆的話題。

要知道，黎曼猜想是千禧年七大數(shù)學(xué)難題之一，被譽(yù)為「猜想界的皇冠」。

2000年，黎曼猜想被美國克雷數(shù)學(xué)研究所（Clay Mathematics Institute of Cambridge，CMI）指定為「七大千禧年難題之一」

由于信息量太大，網(wǎng)友們直接被整懵了，分不清這是真的還是在玩?！?/span>

幾個(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ì)此，他用諷刺的語氣調(diào)侃道：「對(duì)對(duì)對(duì)，Grok 3訓(xùn)著訓(xùn)著突然開始攻擊辦公室的保安了?！?/span>

另一位研究人員Heinrich Kuttler也接梗道：「對(duì)對(duì)對(duì)，情況非常糟糕！我們后來用nan（Not a Number，非數(shù)）把所有壞的權(quán)重都替換了一遍，才恢復(fù)。」

網(wǎng)友見狀，也跟著玩起了梗。

要攻克黎曼猜想，還差些什么？

言歸正傳，讓我們來仔細(xì)看一下，目前人類離攻克黎曼猜想還差幾步。

如今，「黎曼猜想」就像是一座巍峨的高峰，165年來從未有人成功攀上。

它就像大海中的燈塔，為數(shù)學(xué)領(lǐng)域的發(fā)展指明方向：很多數(shù)論和復(fù)變函數(shù)領(lǐng)域的工作都基于黎曼猜想為真這個(gè)前提，因此一旦證明了黎曼猜想，許多其他工作也會(huì)得到完整的證明。

黎曼猜想起源于德國數(shù)學(xué)家高斯，他給出了一個(gè)公式，能夠近似地預(yù)測(cè)出任意數(shù)字的素?cái)?shù)個(gè)數(shù)。

在1859年，德國數(shù)學(xué)家波恩哈德·黎曼改進(jìn)了高斯的公式，用涉及復(fù)變量函數(shù)演算的方法，得出一個(gè)原創(chuàng)公式。

這就是赫赫有名的「黎曼猜想」。

根據(jù)公式，能夠畫出無窮多個(gè)點(diǎn)。黎曼猜測(cè)，這些點(diǎn)有一定的排列規(guī)律，一部分在一條橫線上，另一部分則在一條豎線上，所有點(diǎn)都在兩條直線上排列，無一例外。

黎曼ζ函數(shù)可視化

理論上，無法證明是否所有的點(diǎn)都在這兩條線上，但是，只要有一個(gè)點(diǎn)不在，就能推翻黎曼猜想！

現(xiàn)在，數(shù)學(xué)家們已經(jīng)用計(jì)算機(jī)驗(yàn)證了最初的15億個(gè)點(diǎn)，全部符合黎曼猜想。

2022年，張益唐發(fā)表111頁論文，宣布本質(zhì)上已證明朗道-西格爾零點(diǎn)問題——廣義黎曼猜想的一種特殊且弱得多的形式。

雖然是一個(gè)弱一點(diǎn)的形式，但本質(zhì)上已經(jīng)是解決了朗道—西格爾零點(diǎn)問題。

用他的話說就是，關(guān)于零點(diǎn)猜想問題，「大海里的針我沒撈到, 但海底地貌我探得差不多了」。

論文鏈接：https://arxiv.org/abs/2211.02515

2024年，陶哲軒力推MIT數(shù)學(xué)教授Larry Guth和牛津大學(xué)菲爾茲獎(jiǎng)得主James Maynard的一篇新論文，認(rèn)為兩人在證明黎曼猜想方面取得了重大突破。

過程中，他們犧牲了一枚棄子，情況雖然變得更棘手，卻反而離答案更近了。

論文地址：https://arxiv.org/abs/2405.20552

當(dāng)然，盡管我們離完全解決這一猜想還很遙遠(yuǎn)。

AI的數(shù)學(xué)能力，到底什么水平？

這么說起來，目前的AI是否真的有證明黎曼猜想的能力呢？

我們可以來看看，爆火全網(wǎng)的AI證明工具AlphaProof，是如何做出IMO 2024的三道題的。

從某種角度來說，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解題中最酷的想法。

在證明過程中，AlphaProof會(huì)使用到Lean 生成證明，并且每個(gè)Lean證明由一系列策略組成。

因此，Mehta將挑選出對(duì)應(yīng)于這些想法的策略，針對(duì)AlphaProof解決的第 1、2和6題進(jìn)行分析。

問題 1

問題

確定所有實(shí)數(shù)α，使得對(duì)于每一個(gè)正整數(shù)n，整數(shù)?α?+?2α?+?+?nα?是n的倍數(shù)。（注意，?z?表示小于或等于z的最大整數(shù)。例如，??π?=?4 和?2?=?2.9?=2。）

解答

答案是所有偶整數(shù)。

需要注意的是，AlphaProof解決這些問題的方式是，提出許多解答候選者，嘗試證明和反駁每一個(gè)，最終僅為正確答案找到證明。

這里看到的證明是，證明答案是偶整數(shù)集的那個(gè)。

證明偶整數(shù)滿足給定性質(zhì)顯而易見，而這個(gè)證明的難點(diǎn)在于，證明除了偶整數(shù)之外沒有其他α能夠滿足它。

AlphaProof以一種有趣（盡管復(fù)雜）的方式做到這一點(diǎn)：

它首先設(shè)定一個(gè)整數(shù)?，使得 2?=?α?+?2α?。這是成立的，因?yàn)橥ㄟ^將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。接下來，它聲稱（并繼續(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ì)我來說，這一聲明的動(dòng)機(jī)相當(dāng)不直觀，而事實(shí)上一切都能奏效幾乎是神奇的。

AlphaProof的完整解決方案如下：

問題 2

問題

找到所有滿足條件的正整數(shù)對(duì)(a,b)，使得存在正整數(shù)g和N，使得gcd(an+b,bn+a)=g對(duì)于所有整數(shù)n≥N成立。

解答

AlphaProof正確給出 (1,1) 是唯一的解。

為了證明沒有其他解可以成立，它要求我們考慮數(shù)ab+1。它聲稱（并隨后證明）ab+1必須整除g。

suffices:b.1*b.2+1∣Y

需要注意的是，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+1∣1+b和ab+1∣1+a，由此可以得出a=b=1。

這一策略緊密地遵循了人類對(duì)此問題的證明。選擇考慮ab+1是構(gòu)建證明的巧妙想法。

AlphaProof 的完整解決方案如下：

問題 6

問題

設(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，證明過程分為兩部分。

首先，它通過證明f(r)+f(?r)只能是0或某個(gè)單一的其他值來證明c≤2。這部分證明相當(dāng)復(fù)雜，并巧妙地利用了給定的aquaesulian性質(zhì)。

完成這一步后，c可以是1或2。

為了證明 c=2，AlphaProof提出了一個(gè)aquaesulian函數(shù) f(x)=?x+2?x?，使得 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è)不同的值。

use Finset.one_lt_card.2$ by exists@0,V.1.mem_toFinset.2 (by exists-1),2,V.1.mem_toFinset.2 (by exists 1/2)

再次，很多內(nèi)容被壓縮到一行中，但通過exists -1和 exists 1/2展示了兩個(gè)不同的值。

這是一個(gè)值得注意的函數(shù)構(gòu)造，而且相當(dāng)難以找到！在509名參與者中只有5人解決了 P6，值得注意的是Tim Gowers在評(píng)審這個(gè)解決方案時(shí)也嘗試了一下，但沒有找到一個(gè)能給出兩個(gè)不同值的函數(shù)。

畢竟，IMO 2024第六題被稱為「終極boss」，可不是那么輕易就解決掉的。

AlphaProof的完整解決方案如下：

AI距離千禧年難題，還有多遠(yuǎn)？

關(guān)于AI究竟能做什么程度的數(shù)學(xué)題，網(wǎng)友們也就此展開了討論。

很多人認(rèn)為，數(shù)學(xué)將是AI最先突破的領(lǐng)域之一，因?yàn)榇嬖谝粋€(gè)可用的既便宜又快速的反饋循環(huán)。

數(shù)學(xué)具有這樣的特性：你可以以很少的成本，100%去驗(yàn)證你所做的事是否正確。

而相對(duì)于Lean之類的數(shù)學(xué)證明工具來說，AI驗(yàn)證實(shí)驗(yàn)的成本（時(shí)間、精力、金錢、安全）都要高出許多數(shù)量級(jí)。

有網(wǎng)友腦洞大開預(yù)測(cè)道：數(shù)學(xué)前沿運(yùn)動(dòng)的加速，值得人類建更多發(fā)電站！

不過，有一名數(shù)學(xué)家卻在評(píng)論區(qū)現(xiàn)身說法，認(rèn)為并不值得用AI這么做。

在他看來，計(jì)算時(shí)間/成本與問題復(fù)雜性之間的權(quán)衡，值得嚴(yán)肅考慮。

理論上講，用形式語言找到證明是一件很輕松的事，因?yàn)橹恍枰恢彼阉骺赡艿淖C明，直到找到所需陳述結(jié)尾的證明就可以了。

計(jì)算的并行化程度如何，硬件能力有多大，AI工具對(duì)于數(shù)學(xué)問題的優(yōu)化程度如何，都會(huì)決定AI用多長(zhǎng)時(shí)間把證明做出來。

但要說專門建數(shù)據(jù)中心和發(fā)電站，把大量能源用于做數(shù)學(xué)題，他覺得沒有必要——因?yàn)檫@并不是為了數(shù)學(xué)界的利益，而是硅谷大廠們自己的愿景。

不過如果進(jìn)一步設(shè)想，現(xiàn)在的Alphaproof如果變成具有天文數(shù)字計(jì)算資源的定理證明器，我們或許有一天就可以證明「P/NP問題」。

因?yàn)椋魏慰勺C明的定理，都可以通過耐心地使用窮舉法，列舉所有可能的證明來找到。

如果存在一個(gè)有限的、格式良好的公式，該公式具有該定理作為結(jié)果，那么該定理就可以根據(jù)定義證明。

而如果說LLM有什么用處，那就是尋找出令人驚訝的聯(lián)系，以人類搜索之外的方式，應(yīng)用現(xiàn)有工具。

AI通過幫助人類解決引理、檢查錯(cuò)誤、形式化證明，來加速數(shù)學(xué)研究，在肉眼可見的未來幾年內(nèi)，即將成為現(xiàn)實(shí)。

而在去年，微軟亞洲研究院、北大、北航等機(jī)構(gòu)的研究人員，就已經(jīng)通過97個(gè)回合的「蘇格拉底式」嚴(yán)格推理，成功讓GPT-4得出了「P≠NP」的結(jié)論。

而這97輪對(duì)話，可以說構(gòu)建出了一個(gè)極難的NP完全問題，其中一些實(shí)例在時(shí)間復(fù)雜度低于O(2^n)（即窮舉搜索）的情況下是不可解的，也就是說，證明結(jié)論為P≠NP。

論文地址：https://arxiv.org/abs/2309.05689

當(dāng)然，這個(gè)證明過程并不嚴(yán)謹(jǐn)，作者用一個(gè)假設(shè)（假定任意CSP問題的精確算法都有一個(gè)等價(jià)的分治算法），繞過了P≠NP問題的難點(diǎn)。

其實(shí)，像Christian Szegedy這樣的AI專家已經(jīng)做過此類預(yù)測(cè)：到2026年底，AI將成為「超人數(shù)學(xué)家」，解決出黎曼猜想等問題。

離AI解決P/NP問題、黎曼猜想這樣的的千禧年難題，還會(huì)有多遠(yuǎn)呢？

馬斯克曾許諾，用10萬塊H100訓(xùn)練的Grok 3將在年底發(fā)布，應(yīng)該會(huì)令人驚嘆。

而如今，這個(gè)規(guī)模已經(jīng)擴(kuò)展到了20萬臺(tái)，再給一點(diǎn)時(shí)間，說不定Grok 3真能出奇跡。