大多數人聽到“忙碌海狸”時可能不會想到數學。但這些勤奮的小動物象徵著這個錯綜複雜的領域中最令人驚歎的概念之一：並非所有事物都可以計算，無論你多麼努力（或者你有多麼勤奮）。忙碌海狸函式是不可計算的數學表示式的第一個例子。該函式本身很容易解釋：它指的是計算機程式在停止之前可以執行的最大步數，如果該程式有 n 個狀態，其中狀態指的是問題的複雜性。但它的值，稱為 BB(n)，對於所有數量的 n 而言，將永遠無法得知。數學家和理論計算機科學家長期以來一直在思考數學工具在哪個 n 值時會失效：可計算性的極限究竟在哪裡？
40 多年來，許多專家認為 BB(5) 可能超出可計算性的這個極限，因此是無法達到的。但現在，一個名為“忙碌海狸挑戰”的國際合作專案已經成功確定了 BB(5) 的值，並且其計算已透過計算機輔助證明助手進行了正式驗證。根據這項新研究，BB(5) 的神奇數字是 47,176,870，這意味著一個具有五個狀態的程式在停止之前最多可以執行 47,176,870 步——或者它將永遠不會停止。上一次重大的“忙碌海狸”成果發生在 1983 年，當時已故計算機科學家艾倫·布雷迪證明 BB(4) 等於 107。
忙碌海狸深深紮根於數學基礎之中。在 20 世紀，許多專家夢想找到一個基礎，所有數學真理都可以在此基礎上得到證明。但在 1931 年，邏輯學家庫爾特·哥德爾，當時年僅 25 歲，就粉碎了他們的希望。他證明，在數學中不可避免地存在不可證明的陳述——既不能被證明也不能被證偽的陳述。最初，專家們希望這只是一個抽象的結果，沒有重要的應用。但他們錯了。
支援科學新聞報道
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞報道 訂閱。透過購買訂閱，您正在幫助確保有關塑造我們當今世界的發現和想法的具有影響力的故事能夠擁有未來。
數學家現在知道許多不可證明的問題。最早的例子之一是停機問題，它涉及演算法的執行。在 20 世紀 30 年代，艾倫·圖靈發現，沒有演算法可以預測具有特定輸入的計算機程式是會永遠執行還是會在某個時候停止。當時，圖靈正在研究這種計算機的理論模型，現在稱為圖靈機。這種理論機器由一條無限長的磁帶組成，磁帶上標記著 1 和 0，以及一個讀取磁帶、描述磁帶並將其向右或向左移動的磁頭。這種機器理論上可以執行任何型別的計算——就像計算機一樣。
假設您想編寫一個圖靈機程式來乘兩個數字。磁帶上的 1 和 0 則對應於這兩個數字。在計算之前，您為機器定義一定數量的狀態或規則，例如 A、B、C 和 D，以及 HALT。這些狀態決定了圖靈機如何對每個輸入做出反應。例如：如果五狀態機器在狀態 A 中讀取磁帶上的 1，它會將此 1 覆蓋為 0，將磁帶向左移動並切換到狀態 C。因此，對於狀態 A 到 D 中的每一個狀態，都需要兩條指令，具體取決於機器在磁帶上找到的是 1 還是 0。在某些情況下（例如，狀態 B 在讀取 1 時），機器可以切換到 HALT 狀態。在這種情況下，圖靈機停止，計算完成。結果將是那時磁帶上的數字。
正如圖靈所證明的那樣，沒有圖靈機可以確定對於圖靈機的所有可能配置（即所有演算法），它們是否會在某個時候停止。而這就是勤奮的海狸發揮作用的地方。
停機問題
在 1962 年開發的“忙碌海狸遊戲”中，匈牙利數學家蒂博爾·拉多尋找特定大小的最勤奮的圖靈機：具有 n 個狀態的圖靈機在某個時候停止時，可以執行的最大計算步數是多少？
要普遍回答這個問題，您必須解決停機問題。要找到最勤奮的海狸，您需要知道哪些圖靈機會停止（因此在某個步驟停止執行），哪些不會停止。但圖靈表明，知道這一點是不可能的，這意味著忙碌海狸函式 BB(n) 對於所有可能的狀態數都無法計算。
儘管如此，拉多還是確定了 BB 函式的前三個值，儘管在某些情況下付出了巨大的努力。困難的部分原因在於，隨著狀態數 (n) 的增加，可能的圖靈機（計算機演算法）的數量迅速增加。對於兩個輸入值 0 或 1 中的每一個，圖靈機在特定狀態下執行三個不同的步驟
它將輸入替換為輸出（0 或 1）。此步驟有兩種可能的運算。
它將磁帶向右或向左移動。這也包含兩種可能的運算。
它更改為 n 個狀態之一或 HALT 狀態。此步驟需要 n + 1 種可能的運算。
因此，對於每個輸入值和 n 個狀態中的每一個狀態，都有 2 x 2 x (n + 1) 種可能的運算。組合兩個輸入將得到總共 (4n + 4)2n 種不同的可能步驟集，其中每個步驟集代表不同的演算法或不同的圖靈機。如果只允許一個狀態，則已經有 64 種不同的圖靈機。在這些機器中，只有那些在第一個計算步驟後切換到 HALT 狀態的機器才會停止。因為除了 HALT 之外只有另一條規則，如果機器不停止，它將永遠繼續執行該規則。因此，沒有一個停止的圖靈機會超過一個計算步驟，這就是為什麼 BB(1) = 1。
如果您允許兩個狀態，情況會變得稍微複雜一些。在這種情況下，已經有 (4 x 2 + 4) 的四次方，即 20,736 個圖靈機需要檢查。沒有普遍有效的方法來調查哪些圖靈機停止。正如拉多發現的那樣，具有兩個狀態的最長執行程式（最勤奮的海狸）可以執行六個算術步驟，因此 BB(2) = 6。
拉多和他的時任博士生沈林也在 1965 年闡明瞭三個狀態的情況：在 16,777,216 個圖靈機中，那些在某個時候停止的機器最多可以執行 BB(3) = 21 個計算步驟。1963 年，拉多將計算 BB(4) 的嘗試描述為毫無希望的。但20 年後，布雷迪成功確定了 BB(4)：具有四個狀態（或四個規則）的圖靈機的最高計算步數是 107。這仍然是四十年來可以精確確定的忙碌海狸函式的最後一個值。
“忙碌海狸”獵人
在布雷迪的結果釋出後不久，數學界轉向精確計算 BB(5)。專家們於 1984 年在德國城市多特蒙德組織了一場競賽，他們試圖找到該函式的第五個值。參與者正在尋找五狀態圖靈機，這些機器在停止之前執行儘可能多的計算步驟。競賽的獲勝者是計算機科學家烏韋·舒爾特，他找到了一個具有 134,467 個計算步驟的程式。五年後，計算機科學家海納·馬爾克森和于爾根·本特羅克找到了五狀態機器中的一臺，它直到達到 47,176,870 步才停止，從而提出了 BB(5) 的新最小值。然而，無法證明在五狀態圖靈機中沒有潛伏著更勤奮的程式。
忙碌海狸獵人需要證明所有其他機器無限期執行或比第 47,176,870 步更早停止。而且存在大量五狀態圖靈機。要確定 BB(n)，必須清楚地表明某些圖靈機永遠不會停止。例如，您必須證明程式最終會進入一個重複自身的迴圈。更棘手的是證明圖靈機在沒有重複模式的情況下無限期地繼續執行——就像無理數的小數位一樣。
在過去的幾十年裡，尋找執行超過 47,176,870 個計算步驟的停止的五狀態圖靈機一直沒有成功。因此，許多專家懷疑 BB(5) = 47,176,870。但如果沒有確鑿的證據，這僅僅是假設。
出於這個原因，當時的計算機科學博士生特里斯坦·斯特林於 2022 年發起了忙碌海狸挑戰。該專案的目的是收集和檢查所有與忙碌海狸相關的結果。例如，如果有人證明五狀態程式可以無限期執行，他們可以在那裡釋出證明並由計算機輔助證明軟體進行檢查。這使得許多感興趣的人可以協同工作並呈現有效的結果。該專案在本月完成，最終證明 BB(5) 確實是 47,176,870。
因為每個忙碌海狸都對應一個演算法，您可能想知道 BB(5) 實際上在計算什麼。該程式對應於一個遞迴函式，類似於考拉茲猜想中的函式，考拉茲猜想是數論中最大的未解決問題之一。BB(5) 計算輸入 x 的值 (5x + 18) / 3，如果 x 可被 3 整除；如果 x 除以 3 餘數為 1，則計算 (5x + 22) ⁄ 3；如果 x 除以 3 餘數為 2，則程式停止。
而對忙碌海狸的搜尋仍在繼續。具有六個狀態的圖靈機的記錄保持者已經執行了如此多的算術步驟，您需要一種新的算術運算才能以緊湊的方式記錄該數字（10↑↑15，或 10 的 10 的 10 次方，總共 15 次）。此外，越來越多的證據表明 BB(6) 可能無法計算。最能說明問題的是，在2024 年，發現了一臺六狀態圖靈機，它幾乎對應於考拉茲問題。因此，如果要證明這臺機器停止（或永遠執行下去），就相當於解決了考拉茲問題。考拉茲猜想指出，如果您從一個正整數開始並遵循兩個特定規則，您將最終進入一個特定的迴圈。數學家們幾十年來一直試圖解決這個問題，但沒有成功。因此，人們擔心考拉茲問題是數學中不可證明的陳述之一。
在這種情況下，計算 BB(6) 的嘗試將不可避免地註定失敗。計算機科學家斯科特·阿倫森也不太抱希望，正如他在一篇部落格文章中所寫：“如果以及當人工智慧超級智慧接管世界時，他們可以擔心 BB(6) 的值。然後上帝可以擔心 BB(7) 的值。” 也許數學家們真的已經達到了 BB(5) 的可計算極限。但誰知道呢：也許有人會再次設法讓專家們感到驚訝。
本文最初發表於《Spektrum der Wissenschaft》，經許可轉載。