目前已知執行時間最長的五規則圖靈機的視覺化。每一列畫素代表計算中的一步，從左向右移動。黑色方塊表示機器列印了1的位置。最右邊的一列顯示了當圖靈機停止時的計算狀態。

程式設計師通常希望最小化程式碼的執行時間。但在1962年，匈牙利數學家提博爾·拉多提出了相反的問題。他問，一個簡單的計算機程式在終止之前最多能執行多少步驟？拉多將這些效率最高但仍能正常工作的程式稱為“忙碌的海狸”。

自從1984年在《科學美國人》的“計算機娛樂”專欄中流行以來，對於程式設計師和其他數學愛好者來說，尋找這些程式一直是一個極其有趣的謎題。但在過去的幾年裡，忙碌的海狸遊戲已經成為一個研究的物件，因為它與數學中一些最崇高的概念和開放問題產生了聯絡。

最近的工作表明，搜尋長時間執行的計算機程式可以闡明數學知識的狀態，甚至告訴我們什麼是可知的。根據研究人員的說法，“忙碌的海狸”遊戲為評估某些問題的難度提供了一個具體的基準，例如尚未解決的哥德巴赫猜想和黎曼假設。它甚至讓我們看到，數學背後的邏輯基石在哪裡崩潰了。近一個世紀前，邏輯學家庫爾特·哥德爾就證明了這種數學未知領域的存在。但忙碌的海狸遊戲可以顯示它實際上在數軸上的位置，就像一幅描繪世界邊緣的古老地圖。

無法計算的電腦遊戲

“忙碌的海狸”是關於圖靈機的行為的，它是由艾倫·圖靈在1936年構想出來的原始的、理想化的計算機。圖靈機在被分割成無數個正方形的帶上執行操作。它是根據一系列規則來執行的。第一條規則是：

如果正方形包含0，則將其替換為1，向右移動一個正方形並參照規則2。如果正方形包含1，離開1，向左移動一個正方形並參考規則3。

每個規則都有這種分叉的“選擇自己的冒險”風格。有些規則說要回到以前的規則，最終會有一條包含“停止”指令的規則。圖靈證明，只要有正確的指令和足夠的時間，這種簡單的計算機就能進行任何可能的計算。

正如圖靈在1936年指出的，為了計算一些東西，圖靈機最終必須停止——它不能陷入無限迴圈。但他也證明了，沒有可靠的、可重複的方法來區分機器停機和機器簡單地無限迴圈執行，這個事實被稱為停機問題。

“忙碌的海狸”遊戲的問題是：給定一定數量的規則，在圖靈機停止執行之前，它能執行的最大步驟是多少？

在這張未註明日期的照片中，提博爾·拉多發明了忙碌的海狸遊戲，將理論上的不可計算性具體化。

例如，如果只允許一條規則，並且想要確保圖靈機停止，那麼這條規則裡必須包含停止指令。單規則機器的忙碌的海狸數為1，即BB(1) =1。

但只要再增加幾條規則，需要考慮的機器數量馬上就會激增。有兩個規則的6561個可能的機器中，在停止執行之前的最大步驟是6步，也有些乾脆無限迴圈了。這些都不是忙碌的海狸，但你如何確定地排除它們呢？圖靈證明了，沒有辦法自動判斷執行1000步或100萬步的機器最終會不會終止。

這就是為什麼發現忙碌的海狸如此困難的原因。沒有通用的方法來識別使用任意數量的指令執行時間最長的圖靈機，你必須自己弄清楚每一種情況的具體情況。換句話說，“忙碌的海狸”遊戲一般來說是“不可計算的”。

證明BB(2) = 6和BB(3) = 107是非常困難的，因此拉多的學生沈林在1965年獲得了該研究的博士學位。拉多認為BB(4)完全沒有希望了，但這最終在1983年解決了。除此之外，這些值實際上會暴增。研究人員已經確定了一個具有5條規則圖靈機，例如，5規則圖靈機執行47,176,870步才停止，所以BB(5)至少有這麼大。BB(6)至少為7.4×10^36,534。要證明確切的值，需要新的想法和新的見解。

閾值

馬里蘭大學帕克分校的計算機科學家威廉·加斯克說，他對“忙碌海狸的數量實際上無法計算這一普遍概念”更感興趣，而不是對確定忙碌海狸的數量的前景感興趣。他和其他數學家主要感興趣的是，將博弈作為衡量重要數學開放問題難度的標尺，或者用來弄清什麼在數學上是可知的。

例如，哥德巴赫猜想詢問是否每個大於2的偶數都是兩個素數的和。在數論中，證明猜想的真假將是一個劃時代的事件，使數學家們能夠更好地理解質數的分佈。2015年，一個名匿名使用者釋出了一個27條規則的圖靈機程式碼，當且僅當哥德巴赫猜想是假的時候，該程式碼才會停止執行。它的工作原理是向上計算所有大於4的偶數，對於每一個整數，它都會透過將另外兩個相加的所有可能方法來得到這個整數，並檢查這兩個整數對是否為素數。當它找到合適的質數對時，它移到下一個偶數並重復這個過程。如果它發現一個不能用質數對求和的偶數，它就會停止。

執行這個無需動腦筋的機器並不是解決猜想的實際方法，因為在它停止之前，我們無法知道它是否會停止。但忙碌的海狸遊戲為這個問題提供了一些線索。如果計算BB(27)是可能的，這將為我們等待哥德巴赫猜想自動解決的時間提供一個上限。這是因為BB(27)對應的是這個27條規則的圖靈機為了停止而必須執行的最大步驟數。如果我們知道這個數字，我們就可以執行圖靈機這麼多步驟。如果它停在那一點，我們就知道哥德巴赫猜想是假的。但如果它永遠不會停下來，那麼就證明了猜想的正確性。

問題是BB(27)是一個難以理解的巨大數字，更不用說去執行那麼多步驟，在我們的物理宇宙中也根本不可能。然而，這個不可理解的巨大數字仍然是一個精確的數字。

2016年，三位數學家發現了一臺744條規則圖靈機，當且僅當黎曼假設為假時，它才會停止工作。黎曼假設也涉及質數的分佈，是克萊數學研究所價值100萬美元的“千年難題”之一。

當然，BB(744)是一個比BB(27)更大的數字。但是，努力確定一些更簡單的東西，比如BB(5)，實際上可能會出現一些新的數字理論問題，這些問題本身就很有趣。例如，數學家帕斯卡•米歇爾在1993年證明，保持紀錄的5規則圖靈機表現出類似於科拉茨猜想中描述的函式的行為。科拉茨猜想是數論中另一個著名的開放問題。

1931年哥德爾著名的不完全性定理證明，任何一組基本公理，只要能作為數學的邏輯基礎，都註定會有兩種命運，【即要麼公理將不一致，導致矛盾（比如證明0 = 1），或者他們會不完整，無法證明一些真實陳述資料（如2 + 2 = 4）】，支撐幾乎所有的現代數學的公理系統。被稱為ZF集合理論，有它自己的哥德爾邊界。

2016年，研究生亞當·耶迪迪亞和他的導師設計了一個7910條規則的圖靈機，只有在ZF集合理論不一致的情況下，圖靈機才會停止。這意味著BB(7910)是一個避開了ZF集合理論公理的計算。這些公理不能用來證明BB(7910)代表的是一個數而不是另一個數，就像不能證明2 + 2 = 4而不是5一樣。

隨後，瑞婭爾設計了一個更簡單的748規則機器，如果ZF不一致，它就會停止——實質上是將不可知閾值從BB(7,910)移近到BB(748)。俄亥俄州立大學的數學邏輯學家、名譽教授哈維•弗裡德曼表示：“數量並非完全荒謬，這是一件引人注目的事情。”弗裡德曼認為，這個數字還可以進一步降低。無論遠近，這種不可知的閾值確實存在。