|
計算機程序在停止之前，能夠運行多久？一年，十年，百年，千年，還是宇宙的年齡？如果你不知道答案，你并不孤單。這個問題困擾并迷惑了數學家們超過60年。為什么？它與一些數學最古老、最著名的未解問題有著令人驚訝的聯系。它提供了一個窗口，揭示了數學基礎邏輯開始崩潰的地方，甚至可能揭示出人類知識的邊界。  就在去年，經過30年的無進展，終于取得了一項重大突破，但這項發現真正值得注意的地方，不僅僅是結果，更是它發生的奇怪方式。它并不像大多數數學問題那樣被解決，不是由一群在大學里受過高度訓練的研究人員來解決的。而是由一群不太可能的數學愛好者解決的，他們大多沒有正式的學術教育，他們通過一個名為“忙碌海貍挑戰”的網站在線聚集在一起。 這一切始于一位數學家和他發明的一個游戲。當大多數人都在問，“計算機能解決哪些問題？”時， 當時，計算機能解決什么問題是非常清楚的，多虧了艾倫·圖靈。他想出了這些簡單的理論設備，叫做圖靈機，它們正好捕捉到計算的真正含義。  圖靈曾假設，這些簡單的計算機能夠執行任何可能的計算。它們是我們所有現代數字計算機的藍圖，Rado確實找到了一些計算機無法解決的問題，要理解它，我們需要了解圖靈機是如何工作的。 圖靈機由一條無限長的帶子組成，帶子被分成若干單元格。每個單元格中都有一個符號，比如零或一。一個“頭”讀取符號，根據符號的不同，它可以擦除符號，寫入新符號，向左移動或向右移動。每個圖靈機都有一組獨特的規則，這些規則告訴它應該做什么。 例如，第一條規則可能是：“如果讀取到零，就在當前單元格寫一個一，然后向右移動一個單元格，并轉到第二條規則。” 還有一條特殊規則，告訴機器何時停止運行。圖靈機可以有任意固定數量的規則。有些有三條規則，有些有10條規則，有些有100條規則。通常，圖靈機規則越多，它能做的計算就越復雜。 從第一條規則開始，圖靈機最終要么停機，要么一直運行下去。所以圖靈機有兩種類型，停機型和非停機型。Rado將圖靈機按規則數量進行了分類。他將所有1條規則的機器歸為一組，所有2條規則的機器歸為一組，所有3條規則的機器歸為一組，以此類推。 在每組中，有些機器會永遠運行下去，有些會很快停機，有些則會花費更長時間才能停機。其中一臺機器會是最后停機的。這就是Rado感興趣的機器，所有停機機器中運行時間最長的。Rado稱它們為忙碌的海貍，因為它們在帶子上游走。 忙碌海貍在停機之前執行的步驟數稱為它的忙碌海貍數，簡稱BBn。例如，對于1條規則的圖靈機，如果你想確保它停機，你實際上只能有一條規則：無論它讀取到什么，都讓它停機。因此，1條規則圖靈機的忙碌海貍數就是1，因為它只需一步就停機。 獲取BB2稍微復雜一些，因為有6,561種2條規則的機器，但已證明，忙碌海貍數2的機器運行6步后就停機。現在，重要的部分來了。Rado發現，找出忙碌海貍及其忙碌海貍數是不可計算的。沒有通用的算法或公式，計算機無法用來找到它們。找到一個忙碌海貍的唯一方法是逐個檢查每臺機器，看看它們運行多長時間。 他找到了自己想要的東西。Rado把他尋找忙碌海貍的過程變成了一個游戲。玩這個游戲，你必須做兩件事，丟棄所有非停機的機器，然后在剩下的機器中，尋找運行時間最長的那臺。他沒想到的是，這個游戲竟然與一些數學上最著名的未解問題有關，并且成為了一個跨越幾十年的追尋，困擾了幾代數學家。 但忙碌海貍與這些著名問題有什么關系呢？為了理解這一點，我們來看其中的一個問題。 哥德巴赫猜想  哥德巴赫猜想說，每個大于二的偶數都可以表示為兩個質數的和。例如，4是2和2的和，都是質數。28是17和11的和，都是質數。你對任何偶數這樣做都行。這個看似簡單的猜想已經無法證明近300年，但到目前為止，我們知道它對于所有小于 4×101?的偶數成立。 但是，逐個檢查每個偶數并不夠，數學家們需要一個嚴謹的邏輯證明，證明它對所有偶數都成立。這時候，一個忙碌海貍可能派上用場了。假設你寫了一個計算機程序，從4開始，逐個檢查每個偶數，只有在發現一個不能表示為兩個質數和的偶數時才停機。 已證明，這個程序對于27條規則的圖靈機來說是可計算的。但這里有個有趣的部分。如果我們知道BB27的值，我們就能解決哥德巴赫猜想。如果我們的程序停機，那么它必定在BB27步內停機。如果它在這個步數內停機，那么程序就發現了一個不能表示為兩個質數和的偶數。這將證明哥德巴赫猜想是錯的。 但如果機器運行超過BB27步，那么我們就知道它永遠不會停機，因為所有停機機器都在BB27步之前停機。這將證明哥德巴赫猜想是對的。因此，哥德巴赫猜想的解決方法可以歸結為尋找27條規則的忙碌海貍。 還有其他類似的圖靈機，它們可以用來解決數學中的其他未解問題，比如黎曼假設。事實上，任何可以用計算機語言寫出的數學命題都可以通過這種方式證明。令人驚訝的是，做這件事所需要的有限步驟，竟然能告訴我們無窮多的數字的信息。 那么我們在等什么呢？為什么不去找出BB27，然后解決哥德巴赫猜想，以及所有其他未解的數學問題呢？ 為什么尋找忙碌海貍如此困難我們已經看過1條和2條規則的忙碌海貍，但3條規則呢？嗯，3條規則的圖靈機超過500萬個，而4條規則的圖靈機有超過70億個。記住，找一個忙碌海貍的唯一方法就是逐個檢查每臺機器。 這就像在一個巨大的數字干草堆中找一根針，而干草堆的大小隨著規則數量的增加而呈指數級增長。但我們可以通過去掉所有非停機的機器，然后只檢查剩下的機器，讓生活變得更輕松嗎？非停機的機器顯然不是忙碌海貍，因為根據定義，忙碌海貍必須停機。 但圖靈給我們帶來了一個麻煩的驚喜。他證明了，沒有一種可靠的、可重復的方法可以判斷圖靈機是否會停機。如果一臺機器已經運行了100年，它可能會在101年停機，而我們無法判斷，除非等著看它會不會停機。這個結果叫做“停機問題”，我做了一個關于它的完整視頻，鏈接在描述中。這是一個非常酷的結果，盡管它有點麻煩。 所以，看來Rado游戲的兩步都極其困難，第一步是因為停機問題，第二步是因為要搜索的機器實在太多了。但我們至少找到了第三個忙碌海貍嗎？ 在1960年代中期，一位堅韌不拔的數學研究生，在俄勒岡州立大學，他的吉祥物碰巧是“本尼海貍”，開始了他的嘗試。他叫Allen Brady，他意識到，如果他忽略掉大部分機器，例如那些立即停機的機器，他就可以瀏覽完所有500萬個3條規則的圖靈機。 他還認識到，許多非停機的機器很容易辨別，因為它們開始循環，重復執行相同的指令。Brady編寫了這個方法，將顯而易見的非忙碌海貍丟掉，并將其做成了一個計算機程序，但當時的計算機無法處理如此繁重的計算。Brady不得不尋找先進計算機。 但是，Rado和他的研究生Shen Lin已經搶先一步，他們找到了第三個忙碌海貍。它在21步內停機。但Brady沒有放棄希望。他立即開始尋找第四個忙碌海貍。 BB(4)但是有一個問題。四條規則的圖靈機比三條規則的圖靈機能做更復雜的計算。這意味著它們的非停機機器更難以辨認，因為很多非停機機器并不會陷入無限循環，而Brady的程序正好擅長識別這些循環。 然而，盡管如此，兩年后，他還是找到了一臺在107步內停機的四條規則圖靈機。他花費了更多的歲月，艱苦地工作，終于證明這臺機器確實是第四個忙碌海貍。 這時，來到了2024年4月，忙碌海貍挑戰賽，一群數學愛好者們的到來。盡管有近17萬億個五條規則的圖靈機，他們竟然做到了別人無法做到的事。他們找到了第五個忙碌海貍，即BB5。 大約在Brady找到了第四個忙碌海貍20年后，多特蒙德大學舉辦了一場比賽，旨在尋找第五個忙碌海貍。超過100位參賽者參加了這場比賽，但比賽結束時，沒人能夠確定性地找出BB5。 然而，一位參賽者找到了一個在10萬步內停機的機器。這場比賽在《科學美國人》上得到了報道，這也使得這項游戲吸引了新一代數學家的關注，不久之后，這個步數很快突破了200萬步，并把可能的BB5步數推高了。 但所有人都震驚了，當研究生Heiner Marxen和Jurgen Buntrock發現了一個五條規則的機器，它在47,176,870步內停機。這是不是第五個忙碌海貍？他們當時不知道，直到30年后才有答案。 幾十年間進展緩慢，但事情在2021年迎來了突破。一位名叫Tristan Sterin的研究生嘗試了Brady的原始方法，只是稍作改動。像Brady一樣，Sterin寫了一個代碼，篩選掉明顯不是第五個忙碌海貍的機器。 他把剩余的機器全部收集到一個數據庫里，準備進一步檢查。到了2021年12月，數據庫完成，里面有超過8800萬臺機器，8800萬臺可能的忙碌海貍。如果他能證明這些機器中的每一臺要么在47百萬步之前停機，要么永遠不停機，那么他就知道這臺47百萬步的機器真的就是第五個忙碌海貍。 但他該如何從8800萬臺機器中篩選出來呢？ Sterin知道他需要幫助，于是他成立了“忙碌海貍挑戰”，一個任何人都可以加入的在線社區。來自世界各地的約20人開始共同解決這個問題，而且他們大多數人都沒有任何正式的數學訓練，他們只是把數學當作興趣或愛好。 大家開始一點點地剖析這8800萬臺機器，并通過Discord保持進展更新。 但問題是，有些機器幾乎不可能分類。其中有一臺機器，聲名遠播，被大家稱為“骨架#1”。這臺機器的棘手之處在于，它有時表現得完全可預測，有時卻完全不可預測。無法知道它接下來會做什么。 但是經過幾個月的反復碰壁，兩位貢獻者最終成功破解了它。Shawn Ligocki和Pavel Kropitz證明了“骨架#1”最終會陷入一個無限循環，但它需要超過萬億萬億步。終于，他們成功地將它歸類為非停機機器，并把它從可能的忙碌海貍列表中剔除。 然而，大家心中仍然存有疑慮。他們能相信他們寫的代碼嗎？即使他們找到了BB5，程序中的任何小錯誤都可能讓他們的結果毫無價值。他們需要證明代碼沒有任何錯誤。 但是，如何證明數千行代碼沒有錯誤呢？ 正是在這個關鍵時刻，一個新的、不太可能的角色加入了，那就是一個證明檢查器。證明檢查器是程序，如果遇到邏輯錯誤，它不會運行，因此幾乎不可能有錯誤。一個好的證明檢查器程序，能夠毫無疑問地確認，團隊的證明沒有任何錯誤的邏輯。 一位雄心勃勃的大學輟學生，自學成才的程序員mei加入了團隊。mei把“骨架#1”的證明轉化為一種叫做COQ的證明檢查語言，驗證了Ligocki和Kropitz的結果，證明“骨架#1”永遠不會停機。 一點一點地，這座大山開始減小，來自其他參與者的非忙碌海貍證明也逐漸到位，但很多證明仍然沒有轉化為COQ，以確保它們是合法的、沒有錯誤的。 然后，在2024年5月10日，一位神秘的參與者名為mxdys宣布：“BB5的COQ證明完成了。”他們把整個團隊的工作匯集成了一份40,000行的COQ證明。這是忙碌海貍5任務的最后一步。這個來自世界各地的、不太可能的團隊，他們因為對數學的熱愛聚集在一起，終于證明了這臺47百萬步的圖靈機就是第五個忙碌海貍。 這是一個重大的成就，但不幸的是，并不是每個人都能一起慶祝。第四個忙碌海貍的發現者Allen Brady，在證明完成前幾周去世了。他享年90歲。雖然他沒能親眼見證這個里程碑，但他的遺產將永遠與忙碌海貍的故事交織在一起。 那么，接下來呢？BB(6)？ 爆炸性增長BB(6)的尋找過程充滿了技術挑戰和不斷的記錄突破。2022年，肖恩·利戈基（Shawn Ligocki）發現了一臺六規則圖靈機，其運行時間超過了宇宙中原子的數量，這一發現引起了極大的關注。三年后，來自斯洛伐克的計算機科學本科生帕維爾·克羅皮茨（Pavel Kropitz）將BB(6)的搜索作為他的畢業論文項目，開始了自己的探索。 克羅皮茨編寫了搜索程序，并將其運行在大學實驗室的30臺計算機上。在一個月的時間里，他發現了一臺新的機器，其運行時間遠超利戈基的記錄，這臺機器被稱為新的“冠軍”。經過進一步的搜索，他又發現了運行時間超過30,000位數字的機器，這足以填滿大約10頁的紙。這一記錄保持了12年，直到2022年5月，利戈基開始了一項新工作，獲得了更強大的計算機集群支持，并利用這些資源重新啟動了搜索。通過更新的硬件，利戈基很快發現了一臺新機器，打破了克羅皮茨的記錄。 隨著利戈基和克羅皮茨不斷刷新記錄，兩人之間的競爭也變得更加激烈。利戈基和克羅皮茨發現的機器不僅僅比現有的記錄稍微更長，而是達到了一個全新的數字層次。為了理解這些數字的規模，我們需要使用“超指數運算”，這是一種增長非常迅速的數學操作。例如，10 ↑↑ 3 表示
當利戈基第二次打破記錄時，他的機器運行了超過 10 ↑↑ 5 步，克羅皮茨回應以一臺運行了 10 ↑↑ 15 步的機器，創造了一個更高的記錄。此時，數字的規模已經超出了我們傳統的數學表示方式。 在此后的幾個月里，“忙碌海貍挑戰”變成了一個合作項目，更多的數學家和計算機科學家加入進來，開始共享數據和計算資源。最終，mxdys，這個神秘的成員，提出了一個新的 BB(6) 下限，采用了更加復雜的自動化分類方法，分析了成千上萬臺圖靈機。 2024年6月，mxdys發現了一個新的冠軍，它在停機前運行了 10 ↑↑ 10^7 步——這個數字的大小無法用常規數字表示，而是需要使用更復雜的數學符號。盡管克羅皮茨在消息發布時表示接受失去冠軍頭銜，但他也繼續保持在排行榜上，擁有其他記錄。 最終，mxdys通過進一步的突破，提出了一個比此前更為巨大的記錄，使用了“超乘法”（pentation），一種更高級的運算方法，來表示這一結果。這些數字已經變得如此龐大，傳統的數字書寫方法已不再適用，甚至使用冪塔來表示也無法滿足其需求。 |
|
|
