40多年的電腦難題－忙碌海狸難題，被一群業餘愛好者攻破了！數學大佬陶哲軒轉發了這一消息，並欣慰表示：這再一次體現了證明助手對於數學研究的協作是多麼有用。

電腦科學家Scott Aaronson為此還寫了一篇博文，並大肆讚賞：

這個發現是自1983年以來，忙碌海狸函數研究中最重要的進展。

具體而言，人們歷經數十年努力，終於找到了第五個「忙碌海狸」圖靈機：

BB(5) =47,176,870（5狀態圖靈機，能在停下來之前寫下47,176,870個「1」）

圖靈機是一種抽象的計算模型，透過讀取和寫入0和1在無限磁帶上進行計算。

早在40多年前，一群電腦科學家在德國多特蒙德舉行競賽，尋找「忙碌海狸」圖靈機。

找出一個特定的圖靈機，在它停止之前能夠寫下最多的1（我們稱之為忙碌海狸數）。

透過找出特定狀態下能在停止前寫下最多1的圖靈機，我們能更能理解計算理論的邊界。

自從1974年確定了第四個忙碌海狸數後，尋找第五個成了懸而未決的問題。

而現在，來自世界各地的20多名貢獻者（其中大多數人沒有傳統的學術資格） ，使用一款名為Coq證明助手的軟體獲得了結果——47,176,870，該軟體證實數學證明沒有錯誤。

這項成就瞬間令社區沸騰，愛爾蘭梅努斯大學電腦科學家Damien Woods驚嘆：

就像博爾特一樣，我很驚訝他們的速度如此之快！

嗯，快半世紀過去了還算快？只能說這個問題雀食有億點難。

別急，且看這群人如何長江後浪推前浪抓住「第5隻海狸」~

為什麼提出「忙碌海狸」？

要回答這個問題，首先需要簡單了解二進位圖靈機。

1936年，電腦科學之父艾倫‧圖靈提出了圖靈機—

由一個無限長的紙帶，一個讀寫頭（可以讀取和寫入紙帶上的信息），以及一組內部狀態等基本部分組成。

圖靈機的行為由一組規則定義，這些規則可以想像成一張表。表中的每行代表一個規則，每列對應讀寫頭讀取到的符號（0或1）。

每條規則指定了在特定狀態下，讀寫頭遇到0或1時應該執行的操作。操作通常包括：

寫入符號：決定在目前儲存格寫入什麼符號（例如，將0替換為1）。

移動方向：決定讀寫頭是向左移動、向右移動或保持不動。

狀態轉換：決定圖靈機的下一個狀態是什麼。

除了處理0和1的規則外，還有一條特殊規則告訴圖靈機何時停止運作。當圖靈機進入這個狀態時，它就不再執行任何操作，相當於「比賽結束」（這種狀態一般不計算在狀態集合）。

而就在停機問題上，已經有研究觀察到：

有些圖靈機會相對較快地停止，其他的則陷入了很容易發現的無限循環。

這也啟發圖靈提出了著名的「停機問題」：

圖靈機是否會在有限的步驟後停止運行，或者它是否會無限期地運行下去？

他也進一步提到，停機問題沒有通用的解決方案，因為人們永遠無法確定適用於一台機器的方法是否也適用於另一台機器。

對於這個結論，數學家Tibor Radó（以下簡稱拉多）不太滿意，並由此發明了「忙碌的海狸遊戲」。

為了將停機問題的本質提煉成更簡單的形式，拉多提出了一個方法——

將圖靈機根據它們擁有的規則數量進行分組。

例如，一組代表所有隻有一條規則的圖靈機，另一組代表所有有兩條規則的圖靈機，依此類推。

1962年，拉多利用這些有限的圖靈機組定義了「忙碌海狸遊戲」。遊戲的玩法是：

1.選擇一個群組，即確定你的圖靈機將擁有的規則數量。

2.為組中的每台機器提供一個初始狀態全是0的磁帶。

3.觀察這些機器的運作。有些機器可能會無限期地運行下去，而其他的則會在某個時刻停止。

4.在那些最終停止的機器中，有的會很快停止，有的則需要更多步驟。每個組別中會有一個運行時間最長的機器，這台機器被稱為「忙碌海狸」。

5.在有n條規則的組別中，這台「忙碌海狸」在停止之前所執行的步數就是所謂的「忙碌海狸數」BB(n)。

6.遊戲的目標是確定這些BB(n)的確切值。

拉多給這樣「極度低效」的圖靈機取了一個有趣且形象的名字：忙碌海狸（Busy Beaver，取自英語中的諺語as busy as a beaver）。

而這個遊戲也最終引來一眾程式設計師和數學愛好者的瘋狂試玩。

早期吃螃蟹的人

Allen Brady（以下簡稱布雷迪），當時的俄勒岡州立大學數學研究生，成了早期挑戰者之一。

在遊戲推出前，人們已經確定了BB(1) = 1，BB(2) = 6，當時人們正嘗試攻克BB(3)。

布雷迪也投身BB(3)，他編寫了計算機程式來模擬圖靈機的行為，這個程式構建了一種“家譜”，根據圖靈機初始行為的相似性，對具有相同規則數量的機器進行分類。

程式只在機器之間行為差異變得重要時才將家譜樹分成多個分支。如果模擬顯示某分支上的機器會停止或進入無限循環，程式就會剪掉這個分支，排除那些不會無限運作下去的圖靈機。

編寫程式只是第一步，布雷迪需要找到足夠強大的電腦來運行它。

在1964年，這不是一件容易的事。最終，他在90英里外的靈長類研究實驗室找到了一台SDS 920電腦。

只可惜BB(3)進行到一半，拉多的研究生Shen Lin已宣布證明BB(3) = 21，不過布雷迪還是繼續證實了Lin的結果。

畢業後，布雷迪發現了新的非停止圖靈機種類，並給它們起了形象的名字。

1966年，他發現了一個在停止前運行了107步的四規則圖靈機，並推測這可能是第四個忙碌海狸，並最終於1974年證明了沒有其他停止的機器能運行更久。

這是四十多年來人類所知的最後一個忙碌的海狸號碼

1982年，第一次大規模尋找BB(5)）的Dortmund競賽正式舉辦，其中運行時間最長的一台在超過10萬步後停止。

1984年，《科學美國人》對這項比賽的報道激發了新一代研究者的興趣，有一位研究者打破了舊紀錄，他發現的一台機器在超過200萬步後停止。

這項新紀錄也引來當時的研究生Heiner Marxen和Jürgen Buntrock，他們在業餘時間合作研究這個問題，開發了加速圖靈機模擬的數學技術。

儘管未能打破200萬步的紀錄，但後來在1989年，Marxen在一家公司工作時，使用一台功能強大的新計算機重新啟動了他的搜索程序，並意外地發現了一個在4700萬步後停止的圖靈機。

2000年代初，一位名叫Georgi Ivanov Georgiev（化名Skelet）的保加利亞電腦科學家非常接近這個目標。

經過兩年的不懈努力，他開發了一個能夠識別非停止機器新種類的電腦程式。儘管他的程式運行了一周並留下了約100個未解決的圖靈機，但他手工分析後將名單減少到43個。

此後人們一直陷入不斷嘗試。

最終確定BB(5)

2022年，研究生Tristan Stérin發起了“忙碌海狸挑戰”，這是一項線上合作，旨在最終確定BB(5)。

在這之前，Stérin決定在傳統方法的基礎上進行調整，使用布雷迪的家譜方法，並計劃用獨立程序處理永遠運行的機器。

到了2021年底，Stérin編寫了第一步的電腦程序，產生約1.2億台可能的圖靈機清單。

為了幫助分析這些機器，Stérin建立了一個線上介面，使用「時空圖」來視覺化圖靈機的行為。

完成這些後，鑑於個人精力有限，他在偶然的情況下拉來了Shawn Ligocki。

Ligocki向團隊介紹了封閉磁帶語言方法，這是一種30年前的技術，他將其應用於當前的忙碌海狸問題。

他寫了一篇部落格文章介紹這項技術，但最初並不知道如何編寫一個能涵蓋所有情況的程式。

然後，又一位Justin Blanchard加入了項目，他想出瞭如何做到這一點，但他的程序相對緩慢。

於是另外兩個貢獻者找到了讓它運作得更快的方法，這項技術甚至可以處理前文提到的43個未解決圖靈機中的10個。

在取得階段性成果後，BB(5)終於迎來兩個關鍵突破。

第一個是Skelet #1，它在可預測行為和混亂行為之間不斷交替，這種特性使得它非常難以分析和理解。

2023年3月，Ligocki和斯洛伐克貢獻者Pavel Kropitz（不會說英語，使用谷歌翻譯與團隊其他成員交流），使用Marxen和Buntrock（之前挑戰200萬步記錄的兩位學生）30年前的加速模擬科技的一個增強版，最終破解了Skelet #1。

他們發現Skelet #1在超過一兆步驟之後才進入一個異常長的重複週期，遠超過一般無限循環在1,000步內開始重複的常規。

由於Skelet #1的行為極為奇怪，Ligocki在將近五個月的時間裡都不確定他們的證明結果是否正確。

後來，一位21歲自學成才的程式設計師（以「mei」為名）加入了團隊，她透過學習Coq證明助手，將團隊的一些證明翻譯成Coq語言，提高了證明的嚴格性和可靠性。

第二個突破是Skelet #17，研究者必須像破解四層加密的秘密訊息一樣，逐層解析其行為模式，才能證明機器永遠不會停止。

儘管研究生Chris Xu和其他社區貢獻者做了大量工作，但大多數證明尚未翻譯成Coq。

直到2023年4月，一位名為mxdys的神秘新貢獻者加入，並在短短幾週內完成了一個40,000行的Coq證明，證實了BB(5) 的值。

mxdys證明第五台忙碌海狸在4700萬步後停止，確認了Marxen和Buntrock的發現。

Coq專家Yannick Forster審查了證明，他興奮表示：

我仍然感到非常震驚。

故事仍未結束

BB(5)終於確認了，目前相關研究者正在起草一份學術論文，這將是一個補充mxdys的Coq證明的人類可讀版本。

但是，BB(5)已確認，BB(6)還會遠嗎？

mxdys和另一位貢獻者Racheline發現了一個六規則的圖靈機，其停機問題與著名的數學難題“科拉茨猜想”相似。

為了避免讓大家頭疼，這裡不再展開這個猜想，各位看官只需要知道它非常難就行。

以至於著名理論計算機科學家Scott Aaronson發出感慨：

BB(5)也許是我們所知道的最後一個忙碌的海狸號碼

嗯？這話有點耳熟，BB(4)好像也是這樣說的。

參考連結：

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

[2]https://news.ycombinator.com/item?id=40857041

[3]https://scottaaronson.blog/?p=8088