在計算機科學的一個神祕領域，一個長達四十年的難題——忙碌海狸問題，最近被一羣業餘愛好者成功破解。這一成就不僅在學術界引起了轟動，也得到了著名數學家陶哲軒的認可，他在社交媒體上轉發了這一消息，並強調了證明助手在數學研究中的重要性。

計算機科學家Scott Aaronson也對這一發現給予了高度評價，認爲這是自1983年以來，忙碌海狸函數研究中最重要的進展。這一成就標誌着對計算理論邊界的深入理解，也展示了軟件輔助證明在解決複雜數學問題中的潛力。

忙碌海狸問題起源於40多年前的德國多特蒙德，當時計算機科學家們試圖尋找能夠在停止前寫下最多"1"的特定圖靈機。圖靈機是一種抽象的計算模型，由艾倫·圖靈在1936年提出，通過讀取和寫入0和1在無限長的磁帶上進行計算。

1.jpg

2.jpg

1974年，第四個忙碌海狸數被確定後，尋找第五個海狸成了一個懸而未決的問題。現在，一個由20多名來自世界各地的貢獻者組成的在線社區，使用名爲Coq的證明助手軟件，成功驗證了第五個忙碌海狸數BB（5）的值爲47，176，870。

這一成就不僅令社區沸騰，也引起了計算機科學家Damien Woods的驚歎，他將這一進展比作博爾特的速度。儘管這個問題的解決可能不會直接應用於計算機科學的其他領域，但對於參與者來說，這場與數學不可能性的鬥爭本身就是最大的獎勵。

忙碌海狸問題的核心在於理解圖靈機的行爲，特別是它們在停機問題上的表現。圖靈機的行爲由一組規則定義，這些規則可以想象成一張表。每條規則指定了在特定狀態下，讀寫頭遇到0或1時應該執行的操作。

儘管圖靈機可能會陷入無限循環，但確定它們是否會停止運行是一個著名的未解問題。數學家Tibor Radó不滿意這個結論，並由此發明了“忙碌的海狸遊戲”，通過將圖靈機根據它們擁有的規則數量進行分組，來探索停機問題的本質。

早期的研究者，如Allen Brady，通過編寫程序模擬圖靈機的行爲，對這一問題進行了探索。他的工作和其他研究者的發現，爲後來的探索者奠定了基礎。

直到2022年，研究生Tristan Stérin發起了“忙碌海狸挑戰”，這是一個在線合作項目，旨在最終確定BB（5）。通過創新的方法和Coq證明助手的幫助，這個團隊最終成功找到了第五個忙碌海狸。

這一成就不僅是對數學不可能性的挑戰，也是對計算機科學極限的探索。隨着BB（5）的確認，研究者們正在起草一份學術論文，這將是一個補充Coq證明的人類可讀版本。同時，他們也在思考，BB(6)的探索是否將成爲下一個目標。

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