陶哲軒轉贊！40多年「忙碌海貍」數學難題獲突破，4萬行Coq代碼立大功

AIGC動態歡迎閱讀

原標題：陶哲軒轉贊！40多年「忙碌海貍」數學難題獲突破，4萬行Coq代碼立大功
關鍵字：圖靈機,機器,報告,規則,程序
文章來源：新智元
內容字數：0字

內容摘要：

新智元報道編輯：編輯部
【新智元導讀】「忙碌海貍」難題困擾了計算機科學家40多年。如今，來自全球各地20+業余開發者和數學家們，終于取得了突破性進展。他們抓到了第五只忙碌海貍——用Coq輔助證明，得到答案47176870。對此陶哲軒激動地表示，這再次體現了證明助手對數學研究協作的重要性。40多年的計算機難題——「忙碌海貍」難題，今天獲得了重大突破了！
著名數學家陶哲軒轉發了這一消息，欣慰地表示：這再一次體現了證明助手對于數學研究的協作是有多么有用。
計算機科學家Scott Aaronson為此還寫了一篇博文，并稱「這個發現是自1983年以來『忙碌海貍』函數研究中最重要的進展」。
40年前，100多名計算機科學家在西德的多特蒙德市，參加了這樣一場奇怪的競賽，選手需要捕捉一種難以捉摸的目標——忙碌海貍。
這次競賽難度極大，因為只有四只海貍被成功捕獲，第五只忙碌海貍逃脫了。
其實，這些海貍其實是一種看起來簡單、運行時間奇長的計算機程序。這些程序異常活躍，對它們的搜索過程，涉及到了一些最著名的數學未解之謎。
甚至可以說，海貍難題直接根植于一個和計算機科學本身一樣古老的不可解問題。
雖然我們知

原文鏈接：陶哲軒轉贊！40多年「忙碌海貍」數學難題獲突破，4萬行Coq代碼立大功