AIGC動態歡迎閱讀

原標題：40年圖靈機難題被業余玩家攻破，陶哲軒：軟件輔助證明改變數學研究規則
關鍵字：圖靈機,機器,規則,程序,貢獻者
文章來源：量子位
內容字數：0字

內容摘要：

一水 發自 凹非寺量子位 | 公眾號 QbitAI40多年的計算機難題——忙碌海貍難題，被一群業余愛好者攻破了！
數學大佬陶哲軒轉發了這一消息，并欣慰表示：
這再一次體現了證明助手對于數學研究的協作是多么有用。
計算機科學家Scott Aaronson為此還寫了一篇博文，并大肆贊賞：
這個發現是自1983年以來，忙碌海貍函數研究中最重要的進展。
具體而言，人們歷經數十年努力，終于找到了第五個“忙碌海貍”圖靈機：
BB(5) =47,176,870（5狀態圖靈機，能在停下來之前寫下47,176,870個“1”）
圖靈機是一種抽象的計算模型，通過讀取和寫入0和1在無限磁帶上進行計算。
早在40多年前，一群計算機科學家在德國多特蒙德舉行競賽，尋找“忙碌海貍”圖靈機。
找出一個特定的圖靈機，在它停止之前能夠寫下最多的1（我們稱之為忙碌海貍數）。
通過找出特定狀態下能在停止前寫下最多1的圖靈機，我們能更好地理解計算理論的邊界。
自從1974年確定了第四個忙碌海貍數后，尋找第五個成了懸而未決的問題。
而現在，來自世界各地的20多名貢獻者（其中大多數人沒有傳統的學術資格），使用一款名為Coq證明助手

原文鏈接：40年圖靈機難題被業余玩家攻破，陶哲軒：軟件輔助證明改變數學研究規則

聯系作者

文章來源：量子位
作者微信：
作者簡介：