40多年的計(jì)算機(jī)難題——「忙碌海貍」難題，今天獲得了重大突破了！

著名數(shù)學(xué)家陶哲軒轉(zhuǎn)發(fā)了這一消息，欣慰地表示：這再一次體現(xiàn)了證明助手對(duì)于數(shù)學(xué)研究的協(xié)作是有多么有用。

計(jì)算機(jī)科學(xué)家Scott Aaronson為此還寫了一篇博文，并稱「這個(gè)發(fā)現(xiàn)是自1983年以來(lái)『忙碌海貍』函數(shù)研究中最重要的進(jìn)展」。

40年前，100多名計(jì)算機(jī)科學(xué)家在西德的多特蒙德市，參加了這樣一場(chǎng)奇怪的競(jìng)賽，選手需要捕捉一種難以捉摸的目標(biāo)——忙碌海貍。

這次競(jìng)賽難度極大，因?yàn)橹挥兴闹缓Ｘ偙怀晒Σ东@，第五只忙碌海貍逃脫了。

其實(shí)，這些海貍其實(shí)是一種看起來(lái)簡(jiǎn)單、運(yùn)行時(shí)間奇長(zhǎng)的計(jì)算機(jī)程序。這些程序異?；钴S，對(duì)它們的搜索過(guò)程，涉及到了一些最著名的數(shù)學(xué)未解之謎。

甚至可以說(shuō)，海貍難題直接根植于一個(gè)和計(jì)算機(jī)科學(xué)本身一樣古老的不可解問(wèn)題。

雖然我們知道自己無(wú)法戰(zhàn)勝數(shù)學(xué)定律，但我們希望贏得一場(chǎng)戰(zhàn)斗。

——三位參賽者

兩年前，一位名叫Tristan Stérin的研究生建起一個(gè)網(wǎng)站，再次向全世界發(fā)起忙碌海貍挑戰(zhàn)賽。

今天，有團(tuán)隊(duì)宣布——他們成功捕捉到了「第五只忙碌海貍」！這是由20多位來(lái)自世界各地業(yè)余愛好者組成的團(tuán)隊(duì)。

答案是47176870

具體來(lái)說(shuō)，他們驗(yàn)證了一個(gè)名為BB(5)的數(shù)字的真值，這個(gè)數(shù)字量化了第五只海貍的忙碌程度。

獲得這個(gè)結(jié)果的過(guò)程中，團(tuán)隊(duì)使用一個(gè)名為Coq的證明助手軟件，后者可以確保數(shù)學(xué)證明沒有錯(cuò)誤。

圣塔菲研究所的計(jì)算機(jī)科學(xué)家Cristopher Moore這樣評(píng)價(jià)：「他們?yōu)榱诉_(dá)到目標(biāo)所進(jìn)行的社會(huì)學(xué)和數(shù)學(xué)工程，實(shí)在令人印象深刻」

「我驚訝于他們完成得如此之快，」愛爾蘭梅努斯大學(xué)的計(jì)算機(jī)科學(xué)家、Stérin的導(dǎo)師Damien Woods說(shuō)?！高@簡(jiǎn)直達(dá)到了Usain Bolt的水平?！?/span>

可以說(shuō)，尋找忙碌海貍最終是一場(chǎng)為了榮譽(yù)的狩獵。

因?yàn)椋珺B(5)的具體數(shù)值在計(jì)算機(jī)科學(xué)的其他領(lǐng)域并沒有任何用處。

但對(duì)于捕捉忙碌海貍的獵人來(lái)說(shuō)，戰(zhàn)勝數(shù)學(xué)不可能性后取得的勝利，本身就是回報(bào)。

停機(jī)，還是不停機(jī)

牽動(dòng)廣大忙碌海貍獵人的程序，不是用普通編程語(yǔ)言編寫的，而是為圖靈機(jī)編寫的指令。

計(jì)算機(jī)科學(xué)家艾倫·圖靈在1936年設(shè)計(jì)了圖靈機(jī)，從而以數(shù)學(xué)方式為計(jì)算過(guò)程建模。

圖靈機(jī)的計(jì)算方式，是在無(wú)限長(zhǎng)的磁帶上讀取和寫入0和1。磁帶被劃分為多個(gè)方形單元格，一個(gè)「讀寫頭」一次可以操作一個(gè)單元格。

每臺(tái)圖靈機(jī)都有一套獨(dú)特的規(guī)則。

每條規(guī)則規(guī)定了讀寫頭在進(jìn)入一個(gè)新的單元格時(shí)應(yīng)該做什么，取決于它遇到的是0還是1。

這意味著，圖靈機(jī)的指令可以用一個(gè)表格來(lái)總結(jié)，每條規(guī)則占一行，兩列分別對(duì)應(yīng)讀寫頭遇到0和遇到1的情況。

一條規(guī)則可能是：「如果讀到0，將其替換為1，向右移動(dòng)一步，并參照規(guī)則C」，這是第一列。

「如果讀到1，保持不變，向左移動(dòng)一步，并參照規(guī)則A」，這是第二列。

所有規(guī)則都如此，除非某個(gè)特殊規(guī)則告訴機(jī)器何時(shí)停止運(yùn)行。

不過(guò)，雖然圖靈機(jī)有停機(jī)的方法，但并不意味著它會(huì)停。

在最簡(jiǎn)單的情況下，它可能會(huì)陷入一個(gè)無(wú)限循環(huán)中，不斷循環(huán)幾個(gè)狀態(tài)。

是否存在這樣一種方法，可以判斷具有特定規(guī)則集的圖靈機(jī)是會(huì)停機(jī)，還是會(huì)永遠(yuǎn)運(yùn)行下去呢？

這，就是著名的停機(jī)問(wèn)題的本質(zhì)，也是使得海貍難題如此迷人的原因。

圖靈證明了停機(jī)問(wèn)題沒有普遍的解決方案——我們永遠(yuǎn)無(wú)法確定，對(duì)一臺(tái)機(jī)器有效的方法是否對(duì)另一臺(tái)機(jī)器也同樣有效。

好在，停機(jī)問(wèn)題并不總是對(duì)特定的機(jī)器來(lái)說(shuō)很難。

比如下面這個(gè)視頻中，有些機(jī)器會(huì)相對(duì)較快地停機(jī)。

這臺(tái)三規(guī)則圖靈機(jī)在11步后停機(jī)

而有的機(jī)器卻很快陷入了無(wú)限循環(huán)。

這臺(tái)三規(guī)則圖靈機(jī)很快陷入了無(wú)限循環(huán)

我們總會(huì)遇到一些難以輕易分類的圖靈機(jī)——它的運(yùn)行會(huì)很快結(jié)束，還是會(huì)在磁帶上永遠(yuǎn)徘徊？

是的，除非它運(yùn)行足夠長(zhǎng)的時(shí)間，否則我們根本不知道，它會(huì)做什么。

忙碌海貍，在不可知邊緣探索

忙碌海貍的故事，始于數(shù)學(xué)家Tibor Radó。

1895年出生于匈牙利，大學(xué)學(xué)習(xí)的是土木工程。一戰(zhàn)爆發(fā)后，在西伯利亞戰(zhàn)俘營(yíng)的同伴指導(dǎo)下開始學(xué)習(xí)數(shù)學(xué)

后來(lái)他重返校園，在俄亥俄州立大學(xué)任教35年。

關(guān)于停機(jī)問(wèn)題，他對(duì)圖靈的證明并不滿意。

為了將這個(gè)問(wèn)題的本質(zhì)提煉得更簡(jiǎn)單，Radó希望根據(jù)圖靈機(jī)的規(guī)則數(shù)量進(jìn)行分類——所有一規(guī)則圖靈機(jī)為一組，所有二規(guī)則圖靈機(jī)為另一組，依此類推。

如此一來(lái)，雖然會(huì)因圖靈機(jī)可以有任意數(shù)量的規(guī)則而被分成無(wú)限多的組，但由于規(guī)則的組合是有限的，所以每組中的不同機(jī)器數(shù)量也是有限的。

這樣推理，就比考慮所有的機(jī)器容易多了。

在1962年的一篇論文中，Radó基于此提出了「忙碌海貍游戲」。

要進(jìn)行這個(gè)游戲，首先需要選擇一個(gè)組——也就是你機(jī)器的規(guī)則數(shù)量。

給組中的每臺(tái)機(jī)器提供一條每個(gè)單元格都是0的磁帶后，有些機(jī)器會(huì)一直運(yùn)行下去，其余的最終會(huì)停機(jī)。

其中有些會(huì)很快停機(jī)，有些會(huì)花更長(zhǎng)時(shí)間，而有一臺(tái)會(huì)是最后一個(gè)停機(jī)的。每個(gè)組都會(huì)有一個(gè)運(yùn)行時(shí)間最長(zhǎng)的成員，這些特別勤奮的機(jī)器，就被稱為「忙碌海貍」。

在擁有n條規(guī)則的組中，忙碌海貍機(jī)器在停機(jī)前所需的步數(shù)，就是相應(yīng)的忙碌海貍數(shù)BB(n)。而游戲的目標(biāo)，是確定這些數(shù)字的確切值。

仔細(xì)一想就知道，解決「忙碌海貍」需要考慮眾多問(wèn)題。

要成功的話，你必須確定每臺(tái)停機(jī)機(jī)器的運(yùn)行時(shí)間，看看哪臺(tái)花費(fèi)的時(shí)間最長(zhǎng)。你還必須證明所有其他的機(jī)器永遠(yuǎn)不會(huì)停機(jī)。

測(cè)量運(yùn)行時(shí)間當(dāng)然很簡(jiǎn)單，因?yàn)樵谄胀ㄓ?jì)算機(jī)上模擬圖靈機(jī)很容易。

但是，想要證明一臺(tái)機(jī)器永遠(yuǎn)運(yùn)行下去，相當(dāng)于為它解決停機(jī)問(wèn)題的具體版本——在最一般形式下，這幾乎是不可能完成的任務(wù)。

「我們?cè)诓豢芍倪吘夁M(jìn)行探索，」軟件工程師、海貍難題的貢獻(xiàn)者Shawn Ligocki這樣說(shuō)。

但不可知性究竟從哪里開始？

只有幾個(gè)規(guī)則的圖靈機(jī)看起來(lái)非常簡(jiǎn)單。理解一個(gè)可以放在索引卡上的程序有多難？

數(shù)學(xué)研究生的海貍團(tuán)隊(duì)

單一規(guī)則的情況很簡(jiǎn)單，因?yàn)閷?shí)際上只有兩種可能性。

如果規(guī)則告訴圖靈機(jī)在看到0時(shí)停機(jī)，它會(huì)在第一步就停止。任何其他規(guī)則都會(huì)導(dǎo)致機(jī)器永遠(yuǎn)在磁帶上前進(jìn)，因?yàn)樗鼤?huì)在每個(gè)單元格中遇到0。這意味著BB(1) = 1。

除了這個(gè)小海貍，一個(gè)只用鉛筆和紙裝備的獵人很快就會(huì)遇到問(wèn)題。對(duì)于兩規(guī)則的情況，已經(jīng)有超過(guò)6000個(gè)不同的圖靈機(jī)需要考慮；這個(gè)數(shù)字在三規(guī)則時(shí)膨脹到數(shù)百萬(wàn)，在四規(guī)則時(shí)膨脹到數(shù)十億。

手工處理所有這些情況是不可能的?！革@然，你不可能做到這一點(diǎn)，」Ligocki說(shuō)?！讣词鼓隳茏龅剑矝]有人會(huì)相信你?！?/span>

這意味著，這個(gè)根植于計(jì)算基礎(chǔ)的問(wèn)題只能在計(jì)算機(jī)的幫助下解決。

是的，一個(gè)相當(dāng)簡(jiǎn)單的程序足以證明BB(2) = 6，但從BB(3)起，就開始變得困難多了。

而Radó介紹這個(gè)游戲后不久，一小部分研究人員開始了這場(chǎng)狩獵。

Oregon State University的數(shù)學(xué)研究生Allen Brady很快就意識(shí)到，取得進(jìn)展的關(guān)鍵，就是忽略圖靈機(jī)之間不重要的差異。

例如，考慮一個(gè)有許多規(guī)則的圖靈機(jī)，其中第一個(gè)規(guī)則告訴它如果讀取到0就停機(jī)。

「其余那些轉(zhuǎn)換中的內(nèi)容并不重要，因?yàn)樗鼤?huì)立即停機(jī)，」Ligocki說(shuō)。就忙碌海貍游戲而言，這些機(jī)器大多數(shù)是多余的，因此可以直接一次性排除它們。

研究生Brady將這個(gè)過(guò)程，整合到一個(gè)用于模擬圖靈機(jī)的計(jì)算機(jī)程序中。

基于機(jī)器初始行為的相似性，這個(gè)程序?yàn)榫哂邢嗤?guī)則數(shù)量的機(jī)器構(gòu)建了一個(gè)類似家族樹的結(jié)構(gòu)。

只有當(dāng)機(jī)器之間的差異變得相關(guān)時(shí)，程序才會(huì)將樹分成多個(gè)分支，并刪除在模擬中停機(jī)或進(jìn)入無(wú)限循環(huán)的整個(gè)分支。

程序是編出來(lái)了，但找到能運(yùn)行它的計(jì)算機(jī)，在1964年時(shí)并不容易。

終于，Brady獲得了90英里外一個(gè)靈長(zhǎng)類研究實(shí)驗(yàn)室計(jì)算機(jī)的使用權(quán)。

沒想到，工作進(jìn)行到一半，Brady發(fā)現(xiàn)自己被半路截胡了：Radó的研究生Shen Lin已經(jīng)證明了第三個(gè)忙碌海貍數(shù)BB(3) = 21。

Brady并未氣餒，不僅確認(rèn)了Lin的結(jié)果，而且在BB(4)上取得了部分突破——此前，Radó認(rèn)為BB(4)「完全無(wú)望」解決。

BB(4)之所以難解，不僅是因?yàn)閱?wèn)題數(shù)量龐大，更因?yàn)樗臈l規(guī)則的機(jī)器能夠表現(xiàn)出的行為，實(shí)在是太豐富了！

所有不停機(jī)的兩規(guī)則機(jī)器，都會(huì)陷入容易檢測(cè)的無(wú)限循環(huán)。

在三規(guī)則的情況下，有幾十臺(tái)機(jī)器會(huì)永遠(yuǎn)運(yùn)行而不進(jìn)入循環(huán)，而證明這些機(jī)器永不停機(jī)，需要不同的方法。

對(duì)于四規(guī)則的機(jī)器，則有成千上萬(wàn)臺(tái)這種非循環(huán)機(jī)器。

畢業(yè)后，Brady識(shí)別出了一些新的非停機(jī)圖靈機(jī)種類，并給它們起了「影樹」和「尾食龍」之類的奇幻名字。

1966年，他發(fā)現(xiàn)了一臺(tái)四規(guī)則機(jī)器，在停機(jī)前運(yùn)行了107步，他猜測(cè)：這就是難以捉摸的第四個(gè)忙碌海貍。

他的猜想是對(duì)的，但直到1974年，他才證明沒有其他停機(jī)機(jī)器能運(yùn)行得更久。

他在一份內(nèi)部技術(shù)報(bào)告中寫下了證明，但直到九年后，報(bào)告才在學(xué)術(shù)期刊上發(fā)表。

這是人類在超過(guò)40年里，所知道的最后一個(gè)忙碌海貍數(shù)。

第五只忙碌海貍誕生！

Brady發(fā)表證明的那一年，也是多特蒙德比賽——第一次尋找第5個(gè)忙碌海貍的大型競(jìng)賽的那一年。

對(duì)于五規(guī)則機(jī)器，可能的圖靈機(jī)數(shù)量接近17萬(wàn)億。即使以每毫秒一個(gè)的速度列出所有這些機(jī)器，也需要超過(guò)500年。

用Brady家譜方法來(lái)縮小搜索空間仍然必不可少，但程序必須運(yùn)行得非?？欤庞邢Ｍ晒?。

參賽者們各自開發(fā)了自己的程序，并且找到了運(yùn)行時(shí)間最長(zhǎng)的五規(guī)則圖靈機(jī)——最忙的那臺(tái)，在超過(guò)100,000步后停機(jī)。

《科學(xué)美國(guó)人》1984年對(duì)比賽報(bào)道后，不久后就有一位研究者打破了多特蒙德的紀(jì)錄：一臺(tái)機(jī)器在超過(guò)200萬(wàn)步后才停機(jī)。

柏林的研究生Heiner Marxen和Jürgen Buntrock，也開始利用業(yè)余時(shí)間研究這個(gè)問(wèn)題。

幾年后，在1989年Marxen成為了程序員，在公司中獲得了一臺(tái)強(qiáng)大的計(jì)算機(jī)。

竟然憑自己的程序找到了一臺(tái)驚人的機(jī)器，在47176870步后才停機(jī)。

起初，他認(rèn)為代碼中肯定有錯(cuò)誤。

但調(diào)試了幾個(gè)小時(shí)后，他開始有一種奇怪的感覺：自己捕獲到了忙碌海貍。

Buntrock很快復(fù)現(xiàn)了這一結(jié)果，兩人發(fā)表了論文。

雖然Marxen捕獲了忙碌海貍，但證明所有剩余的機(jī)器都不會(huì)停機(jī)，則花了超過(guò)30年。

在2000年初，一位名叫Georgi Ivanov Georgiev的保加利亞計(jì)算機(jī)科學(xué)家?guī)缀醭晒α恕?/span>

當(dāng)時(shí)，他在一家國(guó)有電信公司擔(dān)任系統(tǒng)管理員。他癡迷于BB(5)的研究，花了兩年時(shí)間，每天花數(shù)小時(shí)改進(jìn)一個(gè)可以識(shí)別新型非停機(jī)機(jī)器的程序。

最終的程序有6000行密集且沒有注釋的代碼，運(yùn)行時(shí)間超過(guò)一周。它留下了大約100臺(tái)未決的圖靈機(jī)。

手工分析這些機(jī)器后，他將名單縮減到43臺(tái)。

2003年，Georgiev在網(wǎng)上發(fā)布了成果。

Marxen鼓勵(lì)Georgiev繼續(xù)努力，但兩年的高強(qiáng)度工作已經(jīng)讓他筋疲力盡。

「這段時(shí)間結(jié)束時(shí)，我無(wú)法再產(chǎn)生任何新想法，我非常疲憊?！?/span>

這也是忙碌海貍研究者所共同面臨的困境。

幾十年來(lái)，他們或獨(dú)自或成對(duì)地辛勤工作，卻沒有得到廣泛學(xué)術(shù)界的太多認(rèn)可。但是要完成這項(xiàng)工作，顯然需要集體的努力。

召集所有獵手

召集所有獵手的努力，始于Tristan Stérin。

2000年代末，他最初通過(guò)IM結(jié)識(shí)了一位編程競(jìng)賽愛好者，從而早早精通了計(jì)算機(jī)編程。

但他很快意識(shí)到編程競(jìng)賽的文化，并不適合自己。

2022年，Tristan Stérin發(fā)起了忙碌海貍挑戰(zhàn)賽，這是一項(xiàng)在線合作，旨在最終確定第五個(gè)忙碌海貍數(shù)量的價(jià)值

他表示，「我不是一個(gè)喜歡競(jìng)爭(zhēng)的人。我喜歡看到一個(gè)問(wèn)題，然后花3個(gè)月時(shí)間思考它，而不是只花30分鐘」。

在好奇心的驅(qū)使下，Stérin決定從法國(guó)來(lái)到愛爾蘭攻讀研究生，在那里他與Woods一起研究DNA計(jì)算，即如何使用DNA鏈實(shí)現(xiàn)算法。

2020年夏天，Woods給他發(fā)了一篇關(guān)于「忙碌海貍」的綜述論文，作者是計(jì)算機(jī)科學(xué)家Scott Aaronson。

Stérin立即被這篇文章吸引了。

論文地址：https://dl.acm.org/doi/10.1145/3427361.3427369

在與Woods合作撰寫了一篇關(guān)于大型圖靈機(jī)能力的論文后，他轉(zhuǎn)向研究BB(5)問(wèn)題，并下定決心要最終證明——Marxen和Buntrock的4700萬(wàn)步機(jī)器，確實(shí)是第五個(gè)「忙碌海貍」。

Stérin說(shuō)，「我有強(qiáng)烈的直覺，自己做不到。但我也有一種直覺，這件事是可以做到的」。

論文地址：https://arxiv.org/pdf/2107.12475

從一開始，Stérin就知道，要有結(jié)論性的證明，必須有良好的文檔記錄和可重復(fù)性，因?yàn)槿魏挝⑿〉能浖e(cuò)誤都會(huì)對(duì)整個(gè)研究造成致命打擊。

Georgiev的程序極其復(fù)雜，但其他研究人員發(fā)現(xiàn)它難以解析。

參與「忙碌海貍」挑戰(zhàn)賽的軟件開發(fā)人員Justin Blanchard表示，「當(dāng)你回頭試圖審查代碼時(shí)，你會(huì)馬上放棄。任何新的方法實(shí)際上都得從頭開始」。他曾是一名數(shù)學(xué)專業(yè)的研究生。

Stérin決定在傳統(tǒng)方法的基礎(chǔ)上進(jìn)行一些改進(jìn)。

他首先使用Brady的家族樹（Brady’s family-tree）方法，來(lái)消除冗余的圖靈機(jī)，并識(shí)別出哪些機(jī)器在4700萬(wàn)步內(nèi)停機(jī)。

但與Brady或其后繼者不同的是，Stérin沒有包含任何用于剔除永遠(yuǎn)運(yùn)行的機(jī)器的代碼。

相反，他計(jì)劃使用獨(dú)立的程序來(lái)解決這些問(wèn)題，每種方法對(duì)應(yīng)一個(gè)程序，證明圖靈機(jī)永遠(yuǎn)不會(huì)停機(jī)。

這樣分塊處理任務(wù)，將使合作伙伴更容易獨(dú)立地完成每個(gè)部分，并交叉檢查結(jié)果。

2021年底，Stérin編寫了第一步的計(jì)算機(jī)程序。

它生成了大約1.2億臺(tái)圖靈機(jī)的列表，這些圖靈機(jī)足以確定BB(5)的值——其余的都是冗余的。

在這1.2億臺(tái)圖靈機(jī)中，大約1/4在Marxen和Buntrock的機(jī)器之前就停機(jī)了，剩下的8800萬(wàn)臺(tái)仍在考慮范圍內(nèi)。

為了幫助分析這些圖靈機(jī)，Stérin構(gòu)建了一個(gè)在線界面，用于在「時(shí)空?qǐng)D」上可視化它們的行為，時(shí)空?qǐng)D是由代表0和1的黑白方格組成的二維網(wǎng)格。

圖中的每一行記錄了圖靈機(jī)演化過(guò)程中的一步。

第一行代表第一步后的紙帶狀態(tài)，第二行顯示第二步后的紙帶狀態(tài)，依此類推。

以這種方式查看，Stérin收集的圖靈機(jī)仿佛活了過(guò)來(lái)，展示出令人眼花繚亂的各種不同模式。

要證明Marxen和Buntrock確實(shí)找到了第五個(gè)忙碌海貍，就意味著要證明這些機(jī)器中的每一個(gè)都會(huì)永遠(yuǎn)運(yùn)行下去。

Stérin知道，自己無(wú)法單獨(dú)完成這項(xiàng)任務(wù)。

2022年春天，Stérin和一些早期加入者在獨(dú)立平臺(tái)Discord上，創(chuàng)建了一個(gè)論壇和一個(gè)單獨(dú)的聊天服務(wù)器。

然后，是時(shí)候?qū)ふ邑暙I(xiàn)者了。

「忙碌海貍」的魅力

Shawn Ligocki很快加入了團(tuán)隊(duì)。

也許這是命運(yùn)：他1985年出生在Beaverton，雖然他第一次聽說(shuō)「忙碌海貍」是在2004年，當(dāng)時(shí)在他大學(xué)第一學(xué)期結(jié)束時(shí)。

寒假期間，他和他的父親Terry一起開始研究海貍搜索算法，Terry是勞倫斯伯克利國(guó)家實(shí)驗(yàn)室的一名應(yīng)用數(shù)學(xué)家。

一個(gè)月后，當(dāng)Ligocki回到大學(xué)忙于課程時(shí)，他的父親興奮地打電話給他。

他決定在Brady發(fā)明的原始忙碌海貍游戲的一個(gè)變體上，測(cè)試他們的一個(gè)算法，并發(fā)現(xiàn)了一臺(tái)打破Brady記錄的圖靈機(jī)。

他們聯(lián)系了已經(jīng)退休的Brady，Brady很高興并在他的網(wǎng)站上公布了這個(gè)結(jié)果。

隨之，Shawn Ligocki很快與世界各地的「忙碌海貍」研究人員通過(guò)電子郵件進(jìn)行交流。

有一次難忘的經(jīng)歷發(fā)生在Ligocki大二暑假訪問(wèn)德國(guó)期間，他順道去了柏林與Marxen見面。

忙碌海貍的魅力，伴隨著Ligocki整個(gè)大學(xué)期間，但畢業(yè)找到工作后，生活瑣事讓他分心。

他偶爾會(huì)重新投入忙碌海貍的研究，但從未持續(xù)太久。

2022年初，他建立了一個(gè)在線討論組，幫助研究人員保持聯(lián)系。5月時(shí)，Stérin發(fā)現(xiàn)了這個(gè)郵件列表，并發(fā)出加入忙碌海貍挑戰(zhàn)的邀請(qǐng)。Ligocki毫不猶豫地接受了邀請(qǐng)。

他對(duì)項(xiàng)目的首次貢獻(xiàn)之一，是復(fù)興了Marxen發(fā)明的一種技術(shù)，這是他們16年前在柏林酒吧討論過(guò)的技術(shù)。

這種技術(shù)被稱為「封閉磁帶語(yǔ)言」（the closed tape language）方法。這是一種新方法，用于識(shí)別圖靈機(jī)磁帶上永不停止的模式。

這是識(shí)別循環(huán)程序和許多其他圖靈機(jī)不停機(jī)的基本策略，但「封閉磁帶語(yǔ)言」方法有潛力通過(guò)統(tǒng)一的數(shù)學(xué)框架識(shí)別更廣泛的模式類別。

Ligocki寫了一篇博客文章，向他的新合作者介紹了這項(xiàng)技術(shù)，但盡管理論上的想法非常通用，他并不知道如何編寫一個(gè)涵蓋所有情況的程序。

Justin Blanchard在秋天加入項(xiàng)目后不久，就找到了方法，但他的程序相對(duì)較慢。然后另外兩位貢獻(xiàn)者找到了讓它運(yùn)行更快的方法。

在幾個(gè)月內(nèi)，「封閉磁帶語(yǔ)言」技術(shù)從一個(gè)有前途的想法變成了他們最強(qiáng)大的工具之一。

它甚至可以處理Georgiev的43個(gè)未解決問(wèn)題中的10個(gè)，為紀(jì)念他而被稱為「Skelet圖靈機(jī)」。

怪物「圖靈機(jī)」來(lái)襲

隨著時(shí)間的推移，新的貢獻(xiàn)者們發(fā)現(xiàn)了「忙碌海貍」挑戰(zhàn)，并開始逐步解決問(wèn)題的不同部分。

但許多圖靈機(jī)仍未解決，其中有兩臺(tái)圖靈機(jī)尤其聲名狼藉。

第一臺(tái)是Skelet #1，它在可預(yù)測(cè)和混亂的行為之間不斷交替。

在2023年3月，Ligocki和Pavel Kropitz——一位不會(huì)說(shuō)英語(yǔ)的斯洛伐克貢獻(xiàn)者，通過(guò)谷歌翻譯與團(tuán)隊(duì)其他成員交流——提出了一系列想法，終于破解了它。

使用Marxen和Buntrock 30年前的加速模擬技術(shù)的升級(jí)版，他們發(fā)現(xiàn)秩序與混亂之間的拉鋸戰(zhàn)確實(shí)結(jié)束了，但只有在超過(guò)一萬(wàn)億億步之后。

然后它最終進(jìn)入了一個(gè)異常長(zhǎng)的重復(fù)循環(huán)周期。

實(shí)際上，幾乎所有的無(wú)限循環(huán)在1000步內(nèi)就會(huì)開始重復(fù)；而Skelet #1的循環(huán)超過(guò)了80億步之長(zhǎng)。

這臺(tái)圖靈機(jī)的行為非常詭異，證明過(guò)程融合了許多不同的想法，以至于Ligocki在近5個(gè)月內(nèi)都無(wú)法確定結(jié)果。

不過(guò)，這一不確定重復(fù)周期，被一位新貢獻(xiàn)者打破了——一位21歲的自學(xué)成才的程序員，名叫Maja K?dzio?ka，多數(shù)情況在她只用一個(gè)字mei。

mei在波蘭長(zhǎng)大，并在2021年秋季在華沙大學(xué)學(xué)習(xí)了一個(gè)學(xué)期后輟學(xué)。

隨后，她在一家軟件公司工作了一年多，但越來(lái)越覺得工作令人筋疲力盡，開始尋找更具智力挑戰(zhàn)的工作。

偶然的機(jī)會(huì)，她在軟件Coq中找到了這種興趣，這是一款設(shè)計(jì)用于編碼和驗(yàn)證數(shù)學(xué)證明有效性的軟件。

當(dāng)時(shí)，忙碌海貍挑戰(zhàn)的貢獻(xiàn)者們已經(jīng)在證明中使用計(jì)算機(jī)程序，但就像紙筆證明一樣，計(jì)算機(jī)程序也容易出錯(cuò)。

而在Coq證明中，代碼只有在每一行邏輯上都能從前一行推導(dǎo)出來(lái)時(shí)才能運(yùn)行，這使得錯(cuò)誤幾乎不可能發(fā)生。

對(duì)mei來(lái)說(shuō)，弄清楚如何制作這些證明開始變得像一場(chǎng)游戲。

在學(xué)習(xí)了Coq之后，mei開始尋找一個(gè)開放的問(wèn)題來(lái)測(cè)試它。就在那時(shí)，她發(fā)現(xiàn)了忙碌海貍挑戰(zhàn)。

幾周后，她將團(tuán)隊(duì)的幾項(xiàng)證明用Coq重新編寫，包括Ligocki和Kropitz關(guān)于Skelet #1永不停止的證明——Ligocki終于可以確定這一點(diǎn)了。

突然間，比Stérin強(qiáng)調(diào)的可重復(fù)性更高的嚴(yán)格標(biāo)準(zhǔn)，似乎成為可能。

項(xiàng)目地址：https://github.com/meithecatte/busycoq

而這一切都是由一個(gè)沒有正式訓(xùn)練的人——一個(gè)業(yè)余數(shù)學(xué)家做出來(lái)的。

突破性進(jìn)展

大約在同一時(shí)間，一位名叫Chris Xu的研究生，在第二臺(tái)怪物圖靈機(jī)——Skelet #17上取得了突破。

通常，即使是復(fù)雜的五規(guī)則圖靈機(jī)（five-rule Turing machines），一旦理解了其工作原理，總結(jié)其行為也不難。

通過(guò)研究Skelet #17磁帶上的模式來(lái)理解它，就像解密四層加密的秘密信息一樣：破解一個(gè)代碼只是揭示了另一個(gè)完全不相關(guān)的代碼，并且下面還有兩個(gè)。

Xu必須解密所有這些代碼，才能最終證明這臺(tái)機(jī)器從未停止。

Xu的證明非常出色，但它涉及一些無(wú)人知道，如何用Coq所要求的精確術(shù)語(yǔ)形式化的數(shù)學(xué)直覺。

而且，忙碌海貍挑戰(zhàn)的工作還遠(yuǎn)未完成：雖然Skelet #1和#17是看起來(lái)最難對(duì)付的兩臺(tái)圖靈機(jī)，但還有其他一些圖靈機(jī)需要解決，還有一些只使用低效程序解決的圖靈機(jī)。

這不足以說(shuō)服世界。

在接下來(lái)的幾個(gè)月里，社區(qū)慢慢拼湊出剩余圖靈機(jī)的證明，但大多數(shù)還沒有被翻譯成Coq。

然后在四月，一個(gè)神秘的新貢獻(xiàn)者出現(xiàn)了，他用化名mxdys來(lái)完成這項(xiàng)工作。

團(tuán)隊(duì)中沒有人知道m(xù)xdys的所在地或其他個(gè)人信息。在一次Discord私信交流中，他提到對(duì)數(shù)學(xué)游戲有長(zhǎng)期興趣，但拒絕提供更多關(guān)于他背景的信息。

5月10日，mxdys在Discord服務(wù)器上發(fā)布了一條簡(jiǎn)短的消息：「BB(5)的Coq證明已經(jīng)完成」。

一分鐘后，Stérin回復(fù)了一串七個(gè)感嘆號(hào)。

在幾周內(nèi)，mxdys完善了社區(qū)的技術(shù)，并將他們的結(jié)果綜合成一個(gè)40,000行的Coq證明。

法國(guó)國(guó)家研究院Inria的Coq專家Yannick Forster在審查證明后表示，「這不是一件容易形式化的事，我仍對(duì)此感到驚訝」。

Marxen和Buntrock在30多年前發(fā)現(xiàn)的那臺(tái)在4700萬(wàn)步后停止運(yùn)轉(zhuǎn)的圖靈機(jī)，確實(shí)是第五個(gè)忙碌海貍。

「這個(gè)消息對(duì)我來(lái)說(shuō)非常令人興奮，」Georgiev在一封電子郵件中寫道。「我從未想到這個(gè)問(wèn)題會(huì)在我有生之年得到解決?！?/span>

但對(duì)另一位忙碌海貍挑戰(zhàn)的開創(chuàng)者來(lái)說(shuō)，這個(gè)消息來(lái)得太晚了。

Allen Brady于4月21日去世，距離證明完成不到一個(gè)月，享年90歲。

貢獻(xiàn)人員名單

以下是所有參與這次證明BB(5)=47176870的貢獻(xiàn)人員名單。

下一步探索

忙碌海貍挑戰(zhàn)的參與者們已經(jīng)開始起草一篇正式的學(xué)術(shù)論文，描述他們的成果，并用更易理解的證明來(lái)補(bǔ)充mxdys的Coq證明。

這將需要一些時(shí)間：大多數(shù)圖靈機(jī)通過(guò)多種方法被證明不會(huì)停止，團(tuán)隊(duì)需要決定如何最佳地將這些結(jié)果組合成一個(gè)完整的證明。

與此同時(shí)，部分團(tuán)隊(duì)成員已經(jīng)開始研究下一個(gè)忙碌海貍。

然而就在四天前，mxdys和另一位名為Racheline的貢獻(xiàn)者發(fā)現(xiàn)了BB(6)的一個(gè)似乎無(wú)法逾越的障礙：一個(gè)六規(guī)則圖靈機(jī)，其停機(jī)問(wèn)題類似于一個(gè)著名的數(shù)學(xué)難題——Collatz猜想。

圖靈機(jī)與Collatz猜想之間的聯(lián)系，可以追溯到1993年數(shù)學(xué)家Pascal Michel的一篇論文。

但新發(fā)現(xiàn)的圖靈機(jī)，被稱為「Antihydra」，是迄今為止最小的一個(gè)，似乎在沒有數(shù)學(xué)上的概念性突破的情況下無(wú)法解決。

論文地址：https://link.springer.com/article/10.1007/BF01409968

顯然，可以想象的到，BB(5)將是我們所知道的最后一個(gè)忙碌海貍的數(shù)字。

忙碌海貍問(wèn)題有許多不同的變種，一些忙碌海貍挑戰(zhàn)的參與者計(jì)劃繼續(xù)研究這些變種。但并不是所有人都打算繼續(xù)這項(xiàng)工作。

他們各自因?yàn)椴煌脑騾⑴c到這個(gè)項(xiàng)目中，現(xiàn)在他們的研究道路開始分道揚(yáng)鑣。

Stérin希望開發(fā)軟件工具，以促進(jìn)其他數(shù)學(xué)領(lǐng)域的在線協(xié)作。

他表示，「忙碌海貍挑戰(zhàn)帶給我的是一種非常深刻的信念，它是一種非常有效的研究方式」。