相信很多大家對陶哲軒轉(zhuǎn)贊！40多年「忙碌海貍」數(shù)學難題獲突破，4萬行Coq代碼立大功還不知道吧，今天菲菲就帶你們一起去了解一下~.~！

【新智元導(dǎo)讀】「忙碌海貍」難題困擾了計算機科學家40多年。如今，來自全球各地20+業(yè)余開發(fā)者和數(shù)學家們，終于取得了突破性進展。他們抓到了第五只忙碌海貍——用Coq輔助證明，得到答案47176870。對此陶哲軒激動地表示，這再次體現(xiàn)了證明助手對數(shù)學研究協(xié)作的重要性。

40多年的計算機難題——「忙碌海貍」難題，今天獲得了重大突破了!

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

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

40年前，100多名計算機科學家在西德的多特蒙德市，參加了這樣一場奇怪的競賽，選手需要捕捉一種難以捉摸的目標——忙碌海貍。

這次競賽難度極大，因為只有四只海貍被成功捕獲，第五只忙碌海貍逃脫了。

其實，這些海貍其實是一種看起來簡單、運行時間奇長的計算機程序。這些程序異?；钴S，對它們的搜索過程，涉及到了一些最著名的數(shù)學未解之謎。

甚至可以說，海貍難題直接根植于一個和計算機科學本身一樣古老的不可解問題。

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

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

答案是47176870

具體來說，他們驗證了一個名為BB（5）的數(shù)字的真值，這個數(shù)字量化了第五只海貍的忙碌程度。

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

圣塔菲研究所的計算機科學家Cristopher Moore這樣評價:「他們?yōu)榱诉_到目標所進行的社會學和數(shù)學工程，實在令人印象深刻」

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

可以說，尋找忙碌海貍最終是一場為了榮譽的狩獵。

因為，BB（5）的具體數(shù)值在計算機科學的其他領(lǐng)域并沒有任何用處。

但對于捕捉忙碌海貍的獵人來說，戰(zhàn)勝數(shù)學不可能性后取得的勝利，本身就是回報。

停機，還是不停機

牽動廣大忙碌海貍獵人的程序，不是用普通編程語言編寫的，而是為圖靈機編寫的指令。

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

圖靈機的計算方式，是在無限長的磁帶上讀取和寫入0和1。磁帶被劃分為多個方形單元格，一個「讀寫頭」一次可以操作一個單元格。

每臺圖靈機都有一套獨特的規(guī)則。

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

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

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

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

所有規(guī)則都如此，除非某個特殊規(guī)則告訴機器何時停止運行。

不過，雖然圖靈機有停機的方法，但并不意味著它會停。

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

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

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

圖靈證明了停機問題沒有普遍的解決方案——我們永遠無法確定，對一臺機器有效的方法是否對另一臺機器也同樣有效。

好在，停機問題并不總是對特定的機器來說很難。

比如下面這個視頻中，有些機器會相對較快地停機。

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

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

我們總會遇到一些難以輕易分類的圖靈機——它的運行會很快結(jié)束，還是會在磁帶上永遠徘徊?

是的，除非它運行足夠長的時間，否則我們根本不知道，它會做什么。

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

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

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

后來他重返校園，在俄亥俄州立大學任教35年。

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

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

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

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

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

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

給組中的每臺機器提供一條每個單元格都是0的磁帶后，有些機器會一直運行下去，其余的最終會停機。

其中有些會很快停機，有些會花更長時間，而有一臺會是最后一個停機的。每個組都會有一個運行時間最長的成員，這些特別勤奮的機器，就被稱為「忙碌海貍」。

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

仔細一想就知道，解決「忙碌海貍」需要考慮眾多問題。

要成功的話，你必須確定每臺停機機器的運行時間，看看哪臺花費的時間最長。你還必須證明所有其他的機器永遠不會停機。

測量運行時間當然很簡單，因為在普通計算機上模擬圖靈機很容易。

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

「我們在不可知的邊緣進行探索，」軟件工程師、海貍難題的貢獻者Shawn Ligocki這樣說。

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

只有幾個規(guī)則的圖靈機看起來非常簡單。理解一個可以放在索引卡上的程序有多難?

數(shù)學研究生的海貍團隊

單一規(guī)則的情況很簡單，因為實際上只有兩種可能性。

如果規(guī)則告訴圖靈機在看到0時停機，它會在第一步就停止。任何其他規(guī)則都會導(dǎo)致機器永遠在磁帶上前進，因為它會在每個單元格中遇到0。這意味著BB（1） =1。

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

手工處理所有這些情況是不可能的。「顯然，你不可能做到這一點，」Ligocki說?！讣词鼓隳茏龅剑矝]有人會相信你。」

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

是的，一個相當簡單的程序足以證明BB（2） =6，但從BB(3)起，就開始變得困難多了。

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

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

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

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

研究生Brady將這個過程，整合到一個用于模擬圖靈機的計算機程序中。

基于機器初始行為的相似性，這個程序為具有相同規(guī)則數(shù)量的機器構(gòu)建了一個類似家族樹的結(jié)構(gòu)。

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

程序是編出來了，但找到能運行它的計算機，在1964年時并不容易。

終于，Brady獲得了90英里外一個靈長類研究實驗室計算機的使用權(quán)。

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

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

BB（4）之所以難解，不僅是因為問題數(shù)量龐大，更因為四條規(guī)則的機器能夠表現(xiàn)出的行為，實在是太豐富了!

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

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

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

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

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

他的猜想是對的，但直到1974年，他才證明沒有其他停機機器能運行得更久。

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

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

第五只忙碌海貍誕生!

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

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

用Brady家譜方法來縮小搜索空間仍然必不可少，但程序必須運行得非?？?，才有希望成功。

參賽者們各自開發(fā)了自己的程序，并且找到了運行時間最長的五規(guī)則圖靈機——最忙的那臺，在超過100，000步后停機。

《科學美國人》1984年對比賽報道后，不久后就有一位研究者打破了多特蒙德的紀錄:一臺機器在超過200萬步后才停機。

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

幾年后，在1989年Marxen成為了程序員，在公司中獲得了一臺強大的計算機。

竟然憑自己的程序找到了一臺驚人的機器，在47176870步后才停機。

起初，他認為代碼中肯定有錯誤。

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

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

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

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

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

最終的程序有6000行密集且沒有注釋的代碼，運行時間超過一周。它留下了大約100臺未決的圖靈機。

手工分析這些機器后，他將名單縮減到43臺。

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

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

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

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

幾十年來，他們或獨自或成對地辛勤工作，卻沒有得到廣泛學術(shù)界的太多認可。但是要完成這項工作，顯然需要集體的努力。

召集所有獵手

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

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

但他很快意識到編程競賽的文化，并不適合自己。

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

他表示，「我不是一個喜歡競爭的人。我喜歡看到一個問題，然后花3個月時間思考它，而不是只花30分鐘」。

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

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

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

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

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

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

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

從一開始，Stérin就知道，要有結(jié)論性的證明，必須有良好的文檔記錄和可重復(fù)性，因為任何微小的軟件錯誤都會對整個研究造成致命打擊。

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

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

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

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

但與Brady或其后繼者不同的是，Stérin沒有包含任何用于剔除永遠運行的機器的代碼。

相反，他計劃使用獨立的程序來解決這些問題，每種方法對應(yīng)一個程序，證明圖靈機永遠不會停機。

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

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

它生成了大約1.2億臺圖靈機的列表，這些圖靈機足以確定BB（5）的值——其余的都是冗余的。

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

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

圖中的每一行記錄了圖靈機演化過程中的一步。

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

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

要證明Marxen和Buntrock確實找到了第五個忙碌海貍，就意味著要證明這些機器中的每一個都會永遠運行下去。

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

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

然后，是時候?qū)ふ邑暙I者了。

「忙碌海貍」的魅力

Shawn Ligocki很快加入了團隊。

也許這是命運:他1985年出生在Beaverton，雖然他第一次聽說「忙碌海貍」是在2004年，當時在他大學第一學期結(jié)束時。

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

一個月后，當Ligocki回到大學忙于課程時，他的父親興奮地打電話給他。

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

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

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

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

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

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

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

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

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

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

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

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

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

它甚至可以處理Georgiev的43個未解決問題中的10個，為紀念他而被稱為「Skelet圖靈機」。

怪物「圖靈機」來襲

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

但許多圖靈機仍未解決，其中有兩臺圖靈機尤其聲名狼藉。

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

在2023年3月，Ligocki和Pavel Kropitz——一位不會說英語的斯洛伐克貢獻者，通過谷歌翻譯與團隊其他成員交流——提出了一系列想法，終于破解了它。

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

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

實際上，幾乎所有的無限循環(huán)在1000步內(nèi)就會開始重復(fù);而Skelet #1的循環(huán)超過了80億步之長。

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

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

mei在波蘭長大，并在2021年秋季在華沙大學學習了一個學期后輟學。

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

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

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

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

對mei來說，弄清楚如何制作這些證明開始變得像一場游戲。

在學習了Coq之后，mei開始尋找一個開放的問題來測試它。就在那時，她發(fā)現(xiàn)了忙碌海貍挑戰(zhàn)。

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

突然間，比Stérin強調(diào)的可重復(fù)性更高的嚴格標準，似乎成為可能。

項目地址:https://github.com/meithecatte/busycoq

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

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

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

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

Xu必須解密所有這些代碼，才能最終證明這臺機器從未停止。

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

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

這不足以說服世界。

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

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

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

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

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

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

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

Marxen和Buntrock在30多年前發(fā)現(xiàn)的那臺在4700萬步后停止運轉(zhuǎn)的圖靈機，確實是第五個忙碌海貍。

「這個消息對我來說非常令人興奮，」Georgiev在一封電子郵件中寫道?！肝覐奈聪氲竭@個問題會在我有生之年得到解決?！?/p>

但對另一位忙碌海貍挑戰(zhàn)的開創(chuàng)者來說，這個消息來得太晚了。

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

以下是所有參與這次證明BB（5）=47176870的貢獻人員名單。

下一步探索

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

這將需要一些時間:大多數(shù)圖靈機通過多種方法被證明不會停止，團隊需要決定如何最佳地將這些結(jié)果組合成一個完整的證明。

與此同時，部分團隊成員已經(jīng)開始研究下一個忙碌海貍。

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

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

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

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

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

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

他們各自因為不同的原因參與到這個項目中，現(xiàn)在他們的研究道路開始分道揚鑣。

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

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

參考資料:

https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/

https://mathstodon.xyz/@TaliaRinger/112719444060361451

以上就是關(guān)于【陶哲軒轉(zhuǎn)贊！40多年「忙碌海貍」數(shù)學難題獲突破，4萬行Coq代碼立大功】的相關(guān)內(nèi)容，希望對大家有幫助！